src/HOL/Orderings.thy
changeset 43597 b4a093e755db
parent 43596 78211f66cf8d
child 43813 07f0650146f2
     1.1 --- a/src/HOL/Orderings.thy	Wed Jun 29 20:39:41 2011 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Wed Jun 29 21:34:16 2011 +0200
     1.3 @@ -534,7 +534,7 @@
     1.4  fun prp t thm = (#prop (rep_thm thm) = t);
     1.5  
     1.6  fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
     1.7 -  let val prems = prems_of_ss ss;
     1.8 +  let val prems = Simplifier.prems_of ss;
     1.9        val less = Const (@{const_name less}, T);
    1.10        val t = HOLogic.mk_Trueprop(le $ s $ r);
    1.11    in case find_first (prp t) prems of
    1.12 @@ -549,7 +549,7 @@
    1.13    handle THM _ => NONE;
    1.14  
    1.15  fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
    1.16 -  let val prems = prems_of_ss ss;
    1.17 +  let val prems = Simplifier.prems_of ss;
    1.18        val le = Const (@{const_name less_eq}, T);
    1.19        val t = HOLogic.mk_Trueprop(le $ r $ s);
    1.20    in case find_first (prp t) prems of
    1.21 @@ -570,7 +570,7 @@
    1.22  
    1.23  fun add_solver name tac =
    1.24    Simplifier.map_simpset_global (fn ss => ss addSolver
    1.25 -    mk_solver name (fn ss => tac (Simplifier.the_context ss) (prems_of_ss ss)));
    1.26 +    mk_solver name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of ss)));
    1.27  
    1.28  in
    1.29    add_simprocs [