simproc bug fix: only TYPING assumptions are given to the simplifier
authorpaulson
Fri Aug 18 12:34:48 2000 +0200 (2000-08-18)
changeset 964989155e48fa53
parent 9648 35d761c7d934
child 9650 6f0b89f2a1f9
simproc bug fix: only TYPING assumptions are given to the simplifier
src/ZF/arith_data.ML
     1.1 --- a/src/ZF/arith_data.ML	Fri Aug 18 12:34:13 2000 +0200
     1.2 +++ b/src/ZF/arith_data.ML	Fri Aug 18 12:34:48 2000 +0200
     1.3 @@ -58,16 +58,19 @@
     1.4                         else FOLogic.mk_iff(t,u);
     1.5  
     1.6  
     1.7 +fun is_eq_thm th = can FOLogic.dest_eq (#prop (rep_thm th));
     1.8 +
     1.9  fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
    1.10  
    1.11  fun prove_conv name tacs sg hyps (t,u) =
    1.12    if t aconv u then None
    1.13    else
    1.14 -  let val ct = add_chyps hyps
    1.15 +  let val hyps' = filter is_eq_thm hyps
    1.16 +      val ct = add_chyps hyps'
    1.17                    (cterm_of sg (FOLogic.mk_Trueprop (mk_eq_iff(t, u))))
    1.18    in Some
    1.19 -      (hyps MRS 
    1.20 -       (prove_goalw_cterm_nocheck [] ct 
    1.21 +      (hyps' MRS 
    1.22 +       (prove_goalw_cterm [] ct 
    1.23  	(fn prems => cut_facts_tac prems 1 :: tacs)))
    1.24        handle ERROR => 
    1.25  	(warning 
    1.26 @@ -155,7 +158,7 @@
    1.27   (open CancelNumeralsCommon
    1.28    val prove_conv = prove_conv "nateq_cancel_numerals"
    1.29    val mk_bal   = FOLogic.mk_eq
    1.30 -  val dest_bal = FOLogic.dest_bin "op =" iT
    1.31 +  val dest_bal = FOLogic.dest_eq
    1.32    val bal_add1 = eq_add_iff RS iff_trans
    1.33    val bal_add2 = eq_add_iff RS iff_trans
    1.34    val trans_tac = gen_trans_tac iff_trans