# HG changeset patch
# User wenzelm
# Date 1273953447 -7200
# Node ID 4eba866311df182d2d6b4e8bb0164b14028bf0c8
# Parent  9bec62c1071483976bed82f9610c891c6b198cc0
avoid open Conv;

diff -r 9bec62c10714 -r 4eba866311df src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Sat May 15 21:50:05 2010 +0200
+++ b/src/Tools/coherent.ML	Sat May 15 21:57:27 2010 +0200
@@ -41,17 +41,13 @@
 
 val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
 
-local open Conv in
-
 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 (Thm.symmetric Data.atomize_elimL) then_conv
+  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
        [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
 
-end;
-
 fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
 
 (* Decompose elimination rule of the form