equal
deleted
inserted
replaced
293 |
293 |
294 parse_translation (advanced) {* |
294 parse_translation (advanced) {* |
295 let |
295 let |
296 fun fun_tr ctxt [cs] = |
296 fun fun_tr ctxt [cs] = |
297 let |
297 let |
298 val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT); |
298 (* FIXME proper name context!? *) |
|
299 val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT); |
299 val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs]; |
300 val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs]; |
300 in lambda x ft end |
301 in lambda x ft end |
301 in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end |
302 in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end |
302 *} |
303 *} |
303 |
304 |