src/HOL/Library/Sum_of_Squares/sum_of_squares.ML

           end
       end
   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.                  *)
 
 local