# HG changeset patch
# User berghofe
# Date 1035212971 -7200
# Node ID ec97dfc2bfe0221df333e5da7fb00cef4a7ee140
# Parent  e36798726ca4b11a4951be999c5ae5995cc63e8f
No more explicit manipulation of flex-flex constraints in goals_conv.

diff -r e36798726ca4 -r ec97dfc2bfe0 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Oct 21 17:07:58 2002 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Oct 21 17:09:31 2002 +0200
@@ -921,14 +921,10 @@
       Pretty.string_of (Display.pretty_thms thms));
 
 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
-(*Do not rewrite flex-flex pairs*)
 fun goals_conv pred cv =
   let fun gconv i ct =
         let val (A,B) = Drule.dest_implies ct
-            val (thA,j) = case term_of A of
-                  Const("=?=",_)$_$_ => (reflexive A, i)
-                | _ => (if pred i then cv A else reflexive A, i+1)
-        in  imp_cong' thA (gconv j B) end
+        in imp_cong' (if pred i then cv A else reflexive A) (gconv (i+1) B) end
         handle TERM _ => reflexive ct
   in gconv 1 end;