src/HOL/Nominal/nominal_inductive.ML
changeset 38715 6513ea67d95d
parent 38558 32ad17fe2b9c
child 38795 848be46708dc
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 25 18:19:04 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 25 18:36:22 2010 +0200
     1.3 @@ -40,7 +40,7 @@
     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_i
     1.8 +fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
     1.9    (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
    1.10      fn Const ("Nominal.perm", _) $ _ $ t =>
    1.11           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))