src/HOL/Orderings.thy
changeset 51717 9e7d1c139569
parent 51658 21c10672633b
child 52143 36ffe23b25f8
     1.1 --- a/src/HOL/Orderings.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -597,8 +597,8 @@
     1.4  
     1.5  fun prp t thm = Thm.prop_of thm = t;  (* FIXME aconv!? *)
     1.6  
     1.7 -fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
     1.8 -  let val prems = Simplifier.prems_of ss;
     1.9 +fun prove_antisym_le ctxt ((le as Const(_,T)) $ r $ s) =
    1.10 +  let val prems = Simplifier.prems_of ctxt;
    1.11        val less = Const (@{const_name less}, T);
    1.12        val t = HOLogic.mk_Trueprop(le $ s $ r);
    1.13    in case find_first (prp t) prems of
    1.14 @@ -612,8 +612,8 @@
    1.15    end
    1.16    handle THM _ => NONE;
    1.17  
    1.18 -fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
    1.19 -  let val prems = Simplifier.prems_of ss;
    1.20 +fun prove_antisym_less ctxt (NotC $ ((less as Const(_,T)) $ r $ s)) =
    1.21 +  let val prems = Simplifier.prems_of ctxt;
    1.22        val le = Const (@{const_name less_eq}, T);
    1.23        val t = HOLogic.mk_Trueprop(le $ r $ s);
    1.24    in case find_first (prp t) prems of
    1.25 @@ -628,13 +628,13 @@
    1.26    handle THM _ => NONE;
    1.27  
    1.28  fun add_simprocs procs thy =
    1.29 -  Simplifier.map_simpset_global (fn ss => ss
    1.30 +  map_theory_simpset (fn ctxt => ctxt
    1.31      addsimprocs (map (fn (name, raw_ts, proc) =>
    1.32        Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
    1.33  
    1.34  fun add_solver name tac =
    1.35 -  Simplifier.map_simpset_global (fn ss => ss addSolver
    1.36 -    mk_solver name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of ss)));
    1.37 +  map_theory_simpset (fn ctxt0 => ctxt0 addSolver
    1.38 +    mk_solver name (fn ctxt => tac ctxt (Simplifier.prems_of ctxt)));
    1.39  
    1.40  in
    1.41    add_simprocs [