--- a/src/HOL/Inductive.thy Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Inductive.thy Thu Feb 11 23:00:22 2010 +0100
@@ -301,10 +301,9 @@
fun fun_tr ctxt [cs] =
let
val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
- val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr
- ctxt [x, cs]
+ val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
in lambda x ft end
-in [("_lam_pats_syntax", fun_tr)] end
+in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
*}
end