# HG changeset patch
# User paulson
# Date 966594888 -7200
# Node ID 89155e48fa53c6cff284facdc51df40169e9f598
# Parent  35d761c7d93469969b70407a3b4e397514bc31a1
simproc bug fix: only TYPING assumptions are given to the simplifier

diff -r 35d761c7d934 -r 89155e48fa53 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Fri Aug 18 12:34:13 2000 +0200
+++ b/src/ZF/arith_data.ML	Fri Aug 18 12:34:48 2000 +0200
@@ -58,16 +58,19 @@
                        else FOLogic.mk_iff(t,u);
 
 
+fun is_eq_thm th = can FOLogic.dest_eq (#prop (rep_thm th));
+
 fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
 
 fun prove_conv name tacs sg hyps (t,u) =
   if t aconv u then None
   else
-  let val ct = add_chyps hyps
+  let val hyps' = filter is_eq_thm hyps
+      val ct = add_chyps hyps'
                   (cterm_of sg (FOLogic.mk_Trueprop (mk_eq_iff(t, u))))
   in Some
-      (hyps MRS 
-       (prove_goalw_cterm_nocheck [] ct 
+      (hyps' MRS 
+       (prove_goalw_cterm [] ct 
 	(fn prems => cut_facts_tac prems 1 :: tacs)))
       handle ERROR => 
 	(warning 
@@ -155,7 +158,7 @@
  (open CancelNumeralsCommon
   val prove_conv = prove_conv "nateq_cancel_numerals"
   val mk_bal   = FOLogic.mk_eq
-  val dest_bal = FOLogic.dest_bin "op =" iT
+  val dest_bal = FOLogic.dest_eq
   val bal_add1 = eq_add_iff RS iff_trans
   val bal_add2 = eq_add_iff RS iff_trans
   val trans_tac = gen_trans_tac iff_trans