diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -32,7 +32,7 @@
 (**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
 
 val collect_mem_simproc =
-  Simplifier.simproc @{theory Set} "Collect_mem" ["Collect t"] (fn thy => fn ss =>
+  Simplifier.simproc_global @{theory Set} "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
          let val (u, _, ps) = HOLogic.strip_psplits t
          in case u of
@@ -67,7 +67,7 @@
 val anyt = Free ("t", TFree ("'t", []));
 
 fun strong_ind_simproc tab =
-  Simplifier.simproc_i @{theory HOL} "strong_ind" [anyt] (fn thy => fn ss => fn t =>
+  Simplifier.simproc_global_i @{theory HOL} "strong_ind" [anyt] (fn thy => fn ss => fn t =>
     let
       fun close p t f =
         let val vs = Term.add_vars t []
@@ -320,7 +320,7 @@
 fun to_pred_simproc rules =
   let val rules' = map mk_meta_eq rules
   in
-    Simplifier.simproc_i @{theory HOL} "to_pred" [anyt]
+    Simplifier.simproc_global_i @{theory HOL} "to_pred" [anyt]
       (fn thy => K (lookup_rule thy (prop_of #> Logic.dest_equals) rules'))
   end;