diff -r 7ae4a23b5be6 -r 78211f66cf8d src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Wed Jun 29 18:12:34 2011 +0200 +++ b/src/HOL/Orderings.thy Wed Jun 29 20:39:41 2011 +0200 @@ -570,7 +570,7 @@ fun add_solver name tac = Simplifier.map_simpset_global (fn ss => ss addSolver - mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss))); + mk_solver name (fn ss => tac (Simplifier.the_context ss) (prems_of_ss ss))); in add_simprocs [