src/HOL/Orderings.thy
changeset 43596 78211f66cf8d
parent 42795 66fcc9882784
child 43597 b4a093e755db
--- 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 [