src/Pure/meta_simplifier.ML
changeset 13661 ec97dfc2bfe0
parent 13614 0b91269c0b13
child 13828 fb6ec40dd291
equal deleted inserted replaced
13660:e36798726ca4 13661:ec97dfc2bfe0
   919   handle THM (s, _, thms) =>
   919   handle THM (s, _, thms) =>
   920     error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   920     error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   921       Pretty.string_of (Display.pretty_thms thms));
   921       Pretty.string_of (Display.pretty_thms thms));
   922 
   922 
   923 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   923 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   924 (*Do not rewrite flex-flex pairs*)
       
   925 fun goals_conv pred cv =
   924 fun goals_conv pred cv =
   926   let fun gconv i ct =
   925   let fun gconv i ct =
   927         let val (A,B) = Drule.dest_implies ct
   926         let val (A,B) = Drule.dest_implies ct
   928             val (thA,j) = case term_of A of
   927         in imp_cong' (if pred i then cv A else reflexive A) (gconv (i+1) B) end
   929                   Const("=?=",_)$_$_ => (reflexive A, i)
       
   930                 | _ => (if pred i then cv A else reflexive A, i+1)
       
   931         in  imp_cong' thA (gconv j B) end
       
   932         handle TERM _ => reflexive ct
   928         handle TERM _ => reflexive ct
   933   in gconv 1 end;
   929   in gconv 1 end;
   934 
   930 
   935 (* Rewrite A in !!x1,...,xn. A *)
   931 (* Rewrite A in !!x1,...,xn. A *)
   936 fun forall_conv cv ct =
   932 fun forall_conv cv ct =