# HG changeset patch
# User paulson
# Date 965636912 -7200
# Node ID be095014e72f26ab39f0ebd75bd96bf67f1e6523
# Parent  c1d9500e292780c4e97f42f2bf6f36d57262a859
prove_conv gets an extra argument, so the ZF instantiation can use hyps

diff -r c1d9500e2927 -r be095014e72f src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Mon Aug 07 10:27:35 2000 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Mon Aug 07 10:28:32 2000 +0200
@@ -36,7 +36,8 @@
   val bal_add1: thm
   val bal_add2: thm
   (*proof tools*)
-  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
+  val prove_conv: tactic list -> Sign.sg -> 
+                  thm list -> term * term -> thm option
   val trans_tac: thm option -> tactic (*applies the initial lemma*)
   val norm_tac: tactic                (*proves the initial lemma*)
   val numeral_simp_tac: tactic        (*proves the final theorem*)
@@ -68,7 +69,7 @@
   in  seek terms1 end;
 
 (*the simplification procedure*)
-fun proc sg _ t =
+fun proc sg hyps t =
   let (*first freeze any Vars in the term to prevent flex-flex problems*)
       val rand_s = gensym"_"
       fun mk_inst (var as Var((a,i),T))  = 
@@ -85,7 +86,7 @@
 		       i + #m + j + k == #m + i + (j + k) *)
 	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
 		raise TERM("cancel_numerals", []) 
-	    else Data.prove_conv [Data.norm_tac] sg 
+	    else Data.prove_conv [Data.norm_tac] sg hyps
 			(t', 
 			 Data.mk_bal (newshape(n1,terms1'), 
 				      newshape(n2,terms2')))
@@ -94,13 +95,13 @@
        (if n2<=n1 then 
 	    Data.prove_conv 
 	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
-		Data.numeral_simp_tac] sg
+		Data.numeral_simp_tac] sg hyps
 	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
 				 Data.mk_sum terms2'))
 	else
 	    Data.prove_conv 
 	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
-		Data.numeral_simp_tac] sg
+		Data.numeral_simp_tac] sg hyps
 	       (t', Data.mk_bal (Data.mk_sum terms1', 
 				 newshape(n2-n1,terms2'))))
   end