diff -r dbf831a50e4a -r 9bec62c10714 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/Tools/coherent.ML	Sat May 15 21:50:05 2010 +0200
@@ -46,8 +46,8 @@
 fun rulify_elim_conv ct =
   if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
   else concl_conv (length (Logic.strip_imp_prems (term_of ct)))
-    (rewr_conv (symmetric Data.atomize_elimL) then_conv
-     MetaSimplifier.rewrite true (map symmetric
+    (rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
+     MetaSimplifier.rewrite true (map Thm.symmetric
        [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
 
 end;