# HG changeset patch
# User wenzelm
# Date 1005405917 -3600
# Node ID 7049eead7a50144d42b8b78ceadae6416439bc54
# Parent  f314630235a45f1958e6fbe65d7a50f85b3e4ceb
use Tactic.prove;

diff -r f314630235a4 -r 7049eead7a50 src/ZF/Datatype.ML
--- a/src/ZF/Datatype.ML	Fri Nov 09 23:44:48 2001 +0100
+++ b/src/ZF/Datatype.ML	Sat Nov 10 16:25:17 2001 +0100
@@ -17,7 +17,7 @@
 
 
   val elims = [make_elim InlD, make_elim InrD,   (*for mutual recursion*)
-	       SigmaE, sumE];			 (*allows * and + in spec*)
+               SigmaE, sumE];                    (*allows * and + in spec*)
   end;
 
 
@@ -38,35 +38,32 @@
        zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
 
   val elims = [make_elim QInlD, make_elim QInrD,   (*for mutual recursion*)
-	       QSigmaE, qsumE];			   (*allows * and + in spec*)
+               QSigmaE, qsumE];                    (*allows * and + in spec*)
   end;
 
 structure CoData_Package = 
     Add_datatype_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
                           and Su=Quine_Sum
-			  and Ind_Package = CoInd_Package
-			  and Datatype_Arg = CoData_Arg);
+                          and Ind_Package = CoInd_Package
+                          and Datatype_Arg = CoData_Arg);
 
 
 
 (*Simproc for freeness reasoning: compare datatype constructors for equality*)
 structure DataFree =
 struct
-  (*prove while suppressing timing information*)
-  fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct);
-
   val trace = ref false;
 
   fun mk_new ([],[]) = Const("True",FOLogic.oT)
     | mk_new (largs,rargs) =
-	fold_bal FOLogic.mk_conj
-		 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
+        fold_bal FOLogic.mk_conj
+                 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
 
 
  fun proc sg _ old =
    let val _ = if !trace then writeln ("data_free: OLD = " ^ 
-				       string_of_cterm (cterm_of sg old))
-	       else ()
+                                       string_of_cterm (cterm_of sg old))
+               else ()
        val (lhs,rhs) = FOLogic.dest_eq old
        val (lhead, largs) = strip_comb lhs
        and (rhead, rargs) = strip_comb rhs
@@ -75,22 +72,19 @@
        val lcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, lname))
        and rcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, rname))
        val new = 
-	   if #big_rec_name lcon_info = #big_rec_name rcon_info 
-	       andalso not (null (#free_iffs lcon_info)) then
-	       if lname = rname then mk_new (largs, rargs)
-	       else Const("False",FOLogic.oT)
-	   else raise Match
+           if #big_rec_name lcon_info = #big_rec_name rcon_info 
+               andalso not (null (#free_iffs lcon_info)) then
+               if lname = rname then mk_new (largs, rargs)
+               else Const("False",FOLogic.oT)
+           else raise Match
        val _ = if !trace then 
-		 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
-	       else ()
-       val ct = Thm.cterm_of sg (Logic.mk_equals (old, new))
-       val thm = prove ct 
-		   (fn _ => [rtac iff_reflection 1,
-			     simp_tac (simpset_of Datatype.thy
-  				          addsimps #free_iffs lcon_info) 1])
-	 handle ERROR =>
-	 error("data_free simproc:\nfailed to prove " ^
-	       string_of_cterm ct)
+                 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
+               else ();
+       val goal = Logic.mk_equals (old, new)
+       val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
+           simp_tac (simpset_of Datatype.thy addsimps #free_iffs lcon_info) 1)
+         handle ERROR =>
+         error ("data_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal)
    in Some thm end
    handle _ => None;
 
diff -r f314630235a4 -r 7049eead7a50 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Fri Nov 09 23:44:48 2001 +0100
+++ b/src/ZF/arith_data.ML	Sat Nov 10 16:25:17 2001 +0100
@@ -72,16 +72,11 @@
   if t aconv u then None
   else
   let val hyps' = filter (not o 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 [] ct 
-	(fn prems => cut_facts_tac prems 1 :: tacs)))
+      val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
+        FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
+  in Some (hyps' MRS Tactic.prove sg [] [] goal (K (EVERY tacs)))
       handle ERROR => 
-	(warning 
-	 ("Cancellation failed: no typing information? (" ^ name ^ ")"); 
-	 None)
+	(warning ("Cancellation failed: no typing information? (" ^ name ^ ")"); None)
   end;
 
 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;