# HG changeset patch
# User wenzelm
# Date 1152731954 -7200
# Node ID 90a8d14f3610b5c1af98e389aa091848f85a5d88
# Parent  a25c5d2832398377e79c8e5437afd1034663f937
simplified prove_conv;

diff -r a25c5d283239 -r 90a8d14f3610 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Wed Jul 12 19:59:14 2006 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Wed Jul 12 21:19:14 2006 +0200
@@ -92,14 +92,13 @@
 
 structure Bin_Simprocs =
   struct
-  fun prove_conv tacs sg (hyps: thm list) xs (t, u) =
+  fun prove_conv tacs ctxt (_: thm list) (t, u) =
     if t aconv u then NONE
     else
       let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
-      in SOME (Goal.prove sg xs [] eq (K (EVERY tacs))) end
+      in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end
 
   fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
-  fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
 
   fun prep_simproc (name, pats, proc) =
     Simplifier.simproc (Theory.sign_of (the_context())) name pats proc;
diff -r a25c5d283239 -r 90a8d14f3610 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Wed Jul 12 19:59:14 2006 +0200
+++ b/src/ZF/arith_data.ML	Wed Jul 12 21:19:14 2006 +0200
@@ -12,8 +12,7 @@
   val nat_cancel: simproc list
   (*tools for use in similar applications*)
   val gen_trans_tac: thm -> thm option -> tactic
-  val prove_conv: string -> tactic list -> Proof.context ->
-                  thm list -> string list -> term * term -> thm option
+  val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option
   val simplify_meta_eq: thm list -> simpset -> thm -> thm
   (*debugging*)
   structure EqCancelNumeralsData   : CANCEL_NUMERALS_DATA
@@ -68,13 +67,13 @@
 
 fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
 
-fun prove_conv name tacs ctxt hyps xs (t,u) =
+fun prove_conv name tacs ctxt prems (t,u) =
   if t aconv u then NONE
   else
-  let val hyps' = List.filter (not o is_eq_thm) hyps
-      val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
+  let val prems' = List.filter (not o is_eq_thm) prems
+      val goal = Logic.list_implies (map (#prop o Thm.rep_thm) prems',
         FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
-  in SOME (hyps' MRS Goal.prove ctxt xs [] goal (K (EVERY tacs)))
+  in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
       handle ERROR msg =>
         (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
   end;