equal
deleted
inserted
replaced
299 parse_translation (advanced) {* |
299 parse_translation (advanced) {* |
300 let |
300 let |
301 fun fun_tr ctxt [cs] = |
301 fun fun_tr ctxt [cs] = |
302 let |
302 let |
303 val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT); |
303 val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT); |
304 val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr |
304 val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs]; |
305 ctxt [x, cs] |
|
306 in lambda x ft end |
305 in lambda x ft end |
307 in [("_lam_pats_syntax", fun_tr)] end |
306 in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end |
308 *} |
307 *} |
309 |
308 |
310 end |
309 end |