diff -r 5f898411ce87 -r 5e94dfead1c2 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Sep 09 14:47:41 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Sep 09 20:57:21 2015 +0200
@@ -44,11 +44,15 @@
   th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
 
 fun mk_perm_bool_simproc names =
-  Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
-    fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
-         if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
-         then SOME perm_bool else NONE
-     | _ => NONE);
+  Simplifier.make_simproc @{context} "perm_bool"
+   {lhss = [@{term "perm pi x"}],
+    proc = fn _ => fn _ => fn ct =>
+      (case Thm.term_of ct of
+        Const (@{const_name Nominal.perm}, _) $ _ $ t =>
+          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
+          then SOME perm_bool else NONE
+       | _ => NONE),
+    identifier = []};
 
 fun transp ([] :: _) = []
   | transp xs = map hd xs :: transp (map tl xs);