--- a/src/Sequents/simpdata.ML Wed Jun 29 20:39:41 2011 +0200
+++ b/src/Sequents/simpdata.ML Wed Jun 29 21:34:16 2011 +0200
@@ -59,11 +59,11 @@
@{thm iff_refl}, reflexive_thm];
fun unsafe_solver ss =
- FIRST' [resolve_tac (triv_rls @ prems_of_ss ss), assume_tac];
+ FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), assume_tac];
(*No premature instantiation of variables during simplification*)
fun safe_solver ss =
- FIRST' [fn i => DETERM (match_tac (triv_rls @ prems_of_ss ss) i), eq_assume_tac];
+ FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ss) i), eq_assume_tac];
(*No simprules, but basic infrastructure for simplification*)
val LK_basic_ss =