src/HOL/HOL.thy
changeset 36543 0e7fc5bf38de
parent 36532 fdfc37254090
child 36635 080b755377c0
child 36641 83d4e01ebda5
--- a/src/HOL/HOL.thy	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Apr 29 22:56:32 2010 +0200
@@ -1491,7 +1491,7 @@
 setup {*
   Induct.setup #>
   Context.theory_map (Induct.map_simpset (fn ss => ss
-    setmksimps (Simpdata.mksimps Simpdata.mksimps_pairs #>
+    setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
       map (Simplifier.rewrite_rule (map Thm.symmetric
         @{thms induct_rulify_fallback induct_true_def induct_false_def})))
     addsimprocs