Simplifier no longer aborts on failed congruence proof.
authorballarin
Mon Apr 28 12:01:45 2003 +0200 (2003-04-28)
changeset 139320eb3d91b519a
parent 13931 38d43d168e87
child 13933 b224c2fd4288
Simplifier no longer aborts on failed congruence proof.
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Mon Apr 28 10:33:57 2003 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon Apr 28 12:01:45 2003 +0200
     1.3 @@ -704,11 +704,11 @@
     1.4           is handled when congc is called *)
     1.5        val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
     1.6        val unit = trace_thm "Applying congruence rule:" thm';
     1.7 -      fun err (msg, thm) = (prthm false msg thm; error "Failed congruence proof!")
     1.8 +      fun err (msg, thm) = (trace_thm msg thm; None)
     1.9    in case prover thm' of
    1.10 -       None => err ("Could not prove", thm')
    1.11 +       None => err ("Congruence proof failed.  Could not prove", thm')
    1.12       | Some thm2 => (case check_conv true (beta_eta_conversion t) thm2 of
    1.13 -          None => err ("Should not have proved", thm2)
    1.14 +          None => err ("Congruence proof failed.  Should not have proved", thm2)
    1.15          | Some thm2' =>
    1.16              if op aconv (pairself term_of (dest_equals (cprop_of thm2')))
    1.17              then None else Some thm2')