# HG changeset patch
# User wenzelm
# Date 1182724593 -7200
# Node ID 7316582081968ab22b3de1319d57367528c28c77
# Parent  a9356b40fbd3dc651225567cdfb70edd73d87bb7
made type conv pervasive;
tuned;

diff -r a9356b40fbd3 -r 731658208196 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sun Jun 24 21:15:55 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Jun 25 00:36:33 2007 +0200
@@ -5,7 +5,7 @@
 
 signature COOPER =
  sig
-  val cooper_conv : Proof.context -> Conv.conv
+  val cooper_conv : Proof.context -> conv
   exception COOPER of string * exn
 end;
 
@@ -17,9 +17,7 @@
 exception COOPER of string * exn;
 val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);
 
-fun C f x y = f y x;
-
-val FWD = C (fold (C implies_elim));
+val FWD = Drule.implies_elim_list;
 
 val true_tm = @{cterm "True"};
 val false_tm = @{cterm "False"};