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 = |