changeset 24349 | 0dd8782fb02d |
parent 23734 | 0e11b904b3a3 |
child 24625 | 0398a5e802d3 |
--- a/src/HOL/Inductive.thy Mon Aug 20 18:07:49 2007 +0200 +++ b/src/HOL/Inductive.thy Mon Aug 20 18:10:13 2007 +0200 @@ -141,8 +141,8 @@ fun fun_tr ctxt [cs] = let val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT); - val ft = DatatypeCase.case_tr DatatypePackage.datatype_of_constr ctxt - [x, cs] + val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr + ctxt [x, cs] in lambda x ft end in [("_lam_pats_syntax", fun_tr)] end *}