diff -r 7ae4a23b5be6 -r 78211f66cf8d src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Jun 29 18:12:34 2011 +0200
+++ b/src/FOL/simpdata.ML	Wed Jun 29 20:39:41 2011 +0200
@@ -108,10 +108,10 @@
 
 val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
 
-fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls @ prems),
+fun unsafe_solver ss = FIRST'[resolve_tac (triv_rls @ prems_of_ss ss),
                                  atac, etac @{thm FalseE}];
 (*No premature instantiation of variables during simplification*)
-fun   safe_solver prems = FIRST'[match_tac (triv_rls @ prems),
+fun safe_solver ss = FIRST'[match_tac (triv_rls @ prems_of_ss ss),
                                  eq_assume_tac, ematch_tac [@{thm FalseE}]];
 
 (*No simprules, but basic infastructure for simplification*)