--- a/src/Tools/coherent.ML Fri Dec 17 16:25:21 2010 +0100
+++ b/src/Tools/coherent.ML Fri Dec 17 17:08:56 2010 +0100
@@ -45,7 +45,7 @@
if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct
else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct)))
(Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
- MetaSimplifier.rewrite true (map Thm.symmetric
+ Raw_Simplifier.rewrite true (map Thm.symmetric
[Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);