# HG changeset patch
# User paulson
# Date 864205154 -7200
# Node ID 114704740c86ab3ce64004a02bfac76399b7afc3
# Parent  c93f54759539a27109c1f7d8b4d8f21122fdcfbd
Code tidying: removal of C combinator

diff -r c93f54759539 -r 114704740c86 TFL/thms.sml
--- a/TFL/thms.sml	Wed May 21 10:58:24 1997 +0200
+++ b/TFL/thms.sml	Wed May 21 10:59:14 1997 +0200
@@ -26,12 +26,10 @@
 
    val COND_CONG = if_cong RS eq_reflection;
 
-   fun C f x y = f y x;
-   fun prover thl = [fast_tac HOL_cs 1];
-   val P = C (prove_goal HOL.thy) prover;
+   fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
 
-   val eqT       = P"(x = True) --> x"
-   val rev_eq_mp = P"(x = y) --> y --> x"
-   val simp_thm  = P"(x-->y) --> (x = x') --> (x' --> y)"
+   val eqT       = prove"(x = True) --> x"
+   val rev_eq_mp = prove"(x = y) --> y --> x"
+   val simp_thm  = prove"(x-->y) --> (x = x') --> (x' --> y)"
 
 end;