# HG changeset patch
# User wenzelm
# Date 1255553864 -7200
# Node ID a1b6e8d281ced2c87dae8fb64ff1df01193c95c0
# Parent  ba14400f7f34772b7f3322febcbf9ae35c52bed3
eliminated obsolete C/flip combinator;

diff -r ba14400f7f34 -r a1b6e8d281ce src/HOL/Library/normarith.ML
--- a/src/HOL/Library/normarith.ML	Wed Oct 14 21:14:53 2009 +0200
+++ b/src/HOL/Library/normarith.ML	Wed Oct 14 22:57:44 2009 +0200
@@ -347,7 +347,6 @@
  val concl = Thm.dest_arg o cprop_of
  fun conjunct1 th = th RS @{thm conjunct1}
  fun conjunct2 th = th RS @{thm conjunct2}
- fun C f x y = f y x
 fun real_vector_ineq_prover ctxt translator (ges,gts) = 
  let 
 (*   val _ = error "real_vector_ineq_prover: pause" *)
@@ -370,7 +369,7 @@
   val th11 = hd (Variable.export ctxt' ctxt [fold implies_intr shs th1])
   val cps = map (swap o Thm.dest_equals) (cprems_of th11)
   val th12 = instantiate ([], cps) th11
-  val th13 = fold (C implies_elim) (map (reflexive o snd) cps) th12;
+  val th13 = fold Thm.elim_implies (map (reflexive o snd) cps) th12;
  in hd (Variable.export ctxt' ctxt [th13])
  end 
 in val real_vector_ineq_prover = real_vector_ineq_prover