src/Tools/induct.ML
changeset 38715 6513ea67d95d
parent 37525 a5ac274798fc
child 41228 e1fce873b814
     1.1 --- a/src/Tools/induct.ML	Wed Aug 25 18:19:04 2010 +0200
     1.2 +++ b/src/Tools/induct.ML	Wed Aug 25 18:36:22 2010 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4    | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
     1.5  
     1.6  val rearrange_eqs_simproc =
     1.7 -  Simplifier.simproc
     1.8 +  Simplifier.simproc_global
     1.9      (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
    1.10      (fn thy => fn ss => fn t =>
    1.11        mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t));