src/HOL/Nominal/nominal_inductive2.ML
changeset 38715 6513ea67d95d
parent 38558 32ad17fe2b9c
child 38795 848be46708dc
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 25 18:36:22 2010 +0200
@@ -8,7 +8,8 @@
 
 signature NOMINAL_INDUCTIVE2 =
 sig
-  val prove_strong_ind: string -> string option -> (string * string list) list -> local_theory -> Proof.state
+  val prove_strong_ind: string -> string option -> (string * string list) list ->
+    local_theory -> Proof.state
 end
 
 structure NominalInductive2 : NOMINAL_INDUCTIVE2 =
@@ -43,7 +44,7 @@
 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
   [(perm_boolI_pi, pi)] perm_boolI;
 
-fun mk_perm_bool_simproc names = Simplifier.simproc_i
+fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
   (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
     fn Const ("Nominal.perm", _) $ _ $ t =>
          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))