--- a/src/HOL/Inductive.thy Mon Jun 27 14:56:39 2011 +0200
+++ b/src/HOL/Inductive.thy Mon Jun 27 17:04:04 2011 +0200
@@ -297,7 +297,7 @@
let
(* FIXME proper name context!? *)
val x = Free (singleton (Name.variant_list (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_permissive ctxt [x, cs];
in lambda x ft end
in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
*}