diff -r 8a104c2a186f -r bd4ecd48c21f src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Fri Dec 17 13:12:58 2010 +0100
+++ b/src/HOL/Tools/TFL/rules.ML	Fri Dec 17 13:45:43 2010 +0100
@@ -714,7 +714,7 @@
                  else
                  let val tych = cterm_of thy
                      val ants1 = map tych ants
-                     val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
+                     val ss' = Simplifier.add_prems (map ASSUME ants1) ss
                      val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
                         (false,true,false) (prover used') ss' (tych Q)
                       handle Utils.ERR _ => Thm.reflexive (tych Q)