diff -r c708ea5b109a -r 0dd8782fb02d src/HOL/Inductive.thy
--- 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
 *}