diff -r 66f8cf4f82d9 -r 023a1d1f97bd src/HOL/Inductive.thy
--- 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
 *}