diff -r 11e7ee2ca77f -r e1fce873b814 src/Tools/coherent.ML --- 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);