# HG changeset patch
# User wenzelm
# Date 880558911 -3600
# Node ID 902ee0883861f2f850600d392749024682d0221f
# Parent  5c1bfefd39b76a39367d6557d38ea9fe8819b03e
removed conv_prover;

diff -r 5c1bfefd39b7 -r 902ee0883861 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Wed Nov 26 16:41:25 1997 +0100
+++ b/src/Provers/simplifier.ML	Wed Nov 26 16:41:51 1997 +0100
@@ -17,8 +17,6 @@
   type simproc
   val mk_simproc: string -> cterm list
     -> (Sign.sg -> thm list -> term -> thm option) -> simproc
-  val conv_prover: (term * term -> term) -> thm -> (thm -> thm)
-    -> tactic -> (int -> tactic) -> Sign.sg -> term -> term -> thm
   type simpset
   val empty_ss: simpset
   val rep_ss: simpset ->
@@ -94,25 +92,6 @@
 fun rep_simproc (Simproc args) = args;
 
 
-(* generic conversion prover *)
-
-fun conv_prover mk_eqv eqv_refl mk_meta_eq expand_tac norm_tac sg t u =
-  let
-    val X = Free (gensym "X.", fastype_of t);
-    val goal = Logic.mk_implies (mk_eqv (X, t), mk_eqv (X, u));
-    val pre_result =
-      prove_goalw_cterm [] (cterm_of sg goal)   (*goal: X=t ==> X=u*)
-        (fn prems => [
-          expand_tac,				(*expand u*)
-          ALLGOALS (cut_facts_tac prems),
-          ALLGOALS norm_tac]);			(*normalize both t and u*)
-  in
-    mk_meta_eq (eqv_refl RS pre_result)         (*final result: t==u*)
-  end
-  handle ERROR => error ("The error(s) above occurred while trying to prove " ^
-    (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
-
-
 
 (** simplification sets **)