src/HOL/Orderings.thy
changeset 43596 78211f66cf8d
parent 42795 66fcc9882784
child 43597 b4a093e755db
     1.1 --- a/src/HOL/Orderings.thy	Wed Jun 29 18:12:34 2011 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Wed Jun 29 20:39:41 2011 +0200
     1.3 @@ -570,7 +570,7 @@
     1.4  
     1.5  fun add_solver name tac =
     1.6    Simplifier.map_simpset_global (fn ss => ss addSolver
     1.7 -    mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
     1.8 +    mk_solver name (fn ss => tac (Simplifier.the_context ss) (prems_of_ss ss)));
     1.9  
    1.10  in
    1.11    add_simprocs [