--- a/src/HOL/Nominal/nominal_inductive.ML Tue Jun 02 09:16:19 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Tue Jun 02 09:40:04 2015 +0200
@@ -39,8 +39,8 @@
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_global_i
- (Thm.theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
+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