--- a/src/HOL/Nominal/nominal_inductive.ML Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Aug 25 18:36:22 2010 +0200
@@ -40,7 +40,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))