No more explicit manipulation of flex-flex constraints in goals_conv.
authorberghofe
Mon Oct 21 17:09:31 2002 +0200 (2002-10-21)
changeset 13661ec97dfc2bfe0
parent 13660 e36798726ca4
child 13662 1f8ddc4b371e
No more explicit manipulation of flex-flex constraints in goals_conv.
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Mon Oct 21 17:07:58 2002 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon Oct 21 17:09:31 2002 +0200
     1.3 @@ -921,14 +921,10 @@
     1.4        Pretty.string_of (Display.pretty_thms thms));
     1.5  
     1.6  (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
     1.7 -(*Do not rewrite flex-flex pairs*)
     1.8  fun goals_conv pred cv =
     1.9    let fun gconv i ct =
    1.10          let val (A,B) = Drule.dest_implies ct
    1.11 -            val (thA,j) = case term_of A of
    1.12 -                  Const("=?=",_)$_$_ => (reflexive A, i)
    1.13 -                | _ => (if pred i then cv A else reflexive A, i+1)
    1.14 -        in  imp_cong' thA (gconv j B) end
    1.15 +        in imp_cong' (if pred i then cv A else reflexive A) (gconv (i+1) B) end
    1.16          handle TERM _ => reflexive ct
    1.17    in gconv 1 end;
    1.18