equal
deleted
inserted
replaced
362 parse_translation (advanced) {* |
362 parse_translation (advanced) {* |
363 let |
363 let |
364 fun fun_tr ctxt [cs] = |
364 fun fun_tr ctxt [cs] = |
365 let |
365 let |
366 val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT); |
366 val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT); |
367 val ft = DatatypeCase.case_tr true Datatype.datatype_of_constr |
367 val ft = DatatypeCase.case_tr true Datatype.info_of_constr |
368 ctxt [x, cs] |
368 ctxt [x, cs] |
369 in lambda x ft end |
369 in lambda x ft end |
370 in [("_lam_pats_syntax", fun_tr)] end |
370 in [("_lam_pats_syntax", fun_tr)] end |
371 *} |
371 *} |
372 |
372 |