--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat May 15 21:50:05 2010 +0200
@@ -1272,7 +1272,7 @@
fun subst_conv eqs t =
let
val t' = fold (Thm.cabs o Thm.lhs_of) eqs t
- in Conv.fconv_rule (Thm.beta_conversion true) (fold (C combination) eqs (reflexive t'))
+ in Conv.fconv_rule (Thm.beta_conversion true) (fold (C Thm.combination) eqs (Thm.reflexive t'))
end
(* A wrapper that tries to substitute away variables first. *)