src/HOL/Nominal/nominal_inductive2.ML
changeset 60359 cb8828b859a1
parent 59940 087d81f5213e
child 60642 48dd1cefb4ae
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Jun 02 09:16:19 2015 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Jun 02 09:40:04 2015 +0200
     1.3 @@ -43,8 +43,8 @@
     1.4  fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
     1.5    [(perm_boolI_pi, pi)] perm_boolI;
     1.6  
     1.7 -fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
     1.8 -  (Thm.theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
     1.9 +fun mk_perm_bool_simproc names =
    1.10 +  Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
    1.11      fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
    1.12           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
    1.13           then SOME perm_bool else NONE