Edward Z. Yang wrote: > I'm a little confused by the definition of json_record; > why does it take a (fl : folder ts) as an argument, but then > not use it for anything? I think this question refers to http://hg.impredicative.com/meta/file/e7d64ea0f922/json.ur . In the definition of [json_record] there, I see the argument [fl] used several times.