# HG changeset patch
# User wenzelm
# Date 1433159183 -7200
# Node ID e85ed7a36b2ffec4811659356ee574474fdc7f9a
# Parent  9c94e6a30d29404d4a7d33239c1021a8a4ec13c6
eliminated odd C combinator -- Isabelle/ML usually has canonical argument order;

diff -r 9c94e6a30d29 -r e85ed7a36b2f src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon Jun 01 13:35:16 2015 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon Jun 01 13:46:23 2015 +0200
@@ -868,13 +868,13 @@
   in mainf end
 end
 
-fun C f x y = f y x;
 (* FIXME : This is very bad!!!*)
 fun subst_conv eqs t =
   let
     val t' = fold (Thm.lambda o Thm.lhs_of) eqs t
   in
-    Conv.fconv_rule (Thm.beta_conversion true) (fold (C Thm.combination) eqs (Thm.reflexive t'))
+    Conv.fconv_rule (Thm.beta_conversion true)
+      (fold (fn a => fn b => Thm.combination b a) eqs (Thm.reflexive t'))
   end
 
 (* A wrapper that tries to substitute away variables first.                  *)
diff -r 9c94e6a30d29 -r e85ed7a36b2f src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Mon Jun 01 13:35:16 2015 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Mon Jun 01 13:46:23 2015 +0200
@@ -636,7 +636,7 @@
   in (strip_aabs used f,args)
   end;
 
-fun pbeta_redex M n = can (Utils.C (dest_pbeta_redex []) n) M;
+fun pbeta_redex M n = can (fn t => dest_pbeta_redex [] t n) M;
 
 fun dest_impl tm =
   let val ants = Logic.strip_imp_prems tm
diff -r 9c94e6a30d29 -r e85ed7a36b2f src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Mon Jun 01 13:35:16 2015 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Mon Jun 01 13:46:23 2015 +0200
@@ -567,7 +567,7 @@
     "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
      val bar = Rules.MP (Rules.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
  in {theory = theory, R=R1, SV=SV,
-     rules = fold (Utils.C Rules.MP) (Rules.CONJUNCTS bar) def',
+     rules = fold (fn a => fn b => Rules.MP b a) (Rules.CONJUNCTS bar) def',
      full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
      patterns = pats}
  end;
@@ -794,7 +794,7 @@
                             #2 o USyntax.strip_forall) TCs
            val TClist = map (fn(TC,lvs) => (Rules.SPEC_ALL(Rules.ASSUME(tych TC)),lvs))
                             TCs_locals
-           val th2list = map (Utils.C Rules.SPEC th1 o tych) ylist
+           val th2list = map (fn t => Rules.SPEC (tych t) th1) ylist
            val nlist = map nested TCs
            val triples = Utils.zip3 TClist th2list nlist
            val Pylist = map mk_ih triples
diff -r 9c94e6a30d29 -r e85ed7a36b2f src/HOL/Tools/TFL/utils.ML
--- a/src/HOL/Tools/TFL/utils.ML	Mon Jun 01 13:35:16 2015 +0200
+++ b/src/HOL/Tools/TFL/utils.ML	Mon Jun 01 13:46:23 2015 +0200
@@ -7,7 +7,6 @@
 signature UTILS =
 sig
   exception ERR of {module: string, func: string, mesg: string}
-  val C: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
   val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a
   val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   val pluck: ('a -> bool) -> 'a list -> 'a * 'a list
@@ -24,8 +23,6 @@
 fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
 
 
-fun C f x y = f y x
-
 fun end_itlist f [] = raise (UTILS_ERR "end_itlist" "list too short")
   | end_itlist f [x] = x 
   | end_itlist f (x :: xs) = f x (end_itlist f xs);