src/HOL/Divides.thy
changeset 51717 9e7d1c139569
parent 51299 30b014246e21
child 52398 656e5e171f19
     1.1 --- a/src/HOL/Divides.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Divides.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -1643,12 +1643,12 @@
     1.4    val simps = @{thms arith_simps} @ @{thms rel_simps} @
     1.5      map (fn th => th RS sym) [@{thm numeral_1_eq_1}]
     1.6    fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
     1.7 -    (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps simps))));
     1.8 -  fun binary_proc proc ss ct =
     1.9 +    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))));
    1.10 +  fun binary_proc proc ctxt ct =
    1.11      (case Thm.term_of ct of
    1.12        _ $ t $ u =>
    1.13        (case try (pairself (`(snd o HOLogic.dest_number))) (t, u) of
    1.14 -        SOME args => proc (Simplifier.the_context ss) args
    1.15 +        SOME args => proc ctxt args
    1.16        | NONE => NONE)
    1.17      | _ => NONE);
    1.18  in