core_sos_tac: SUBPROOF body operates on subgoal 1;
tuned;

--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Oct 01 20:20:56 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Oct 01 20:33:45 2009 +0200
@@ -1392,17 +1392,12 @@
               else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs))
 in () end
 
-fun core_sos_tac print_cert prover ctxt i = 
+fun core_sos_tac print_cert prover = SUBPROOF (fn {concl, context, ...} =>
   let
-    fun core_tac {concl, context, ...} =
-      let
-        val _ = check_sos known_sos_constants concl
-        val (ths, certificates) = real_sos prover context (Thm.dest_arg concl)
-        val _ = print_cert certificates
-      in rtac ths i end
-  in
-    SUBPROOF core_tac ctxt i
-  end
+    val _ = check_sos known_sos_constants concl
+    val (ths, certificates) = real_sos prover context (Thm.dest_arg concl)
+    val _ = print_cert certificates
+  in rtac ths 1 end)
 
 fun default_SOME f NONE v = SOME v
   | default_SOME f (SOME v) _ = SOME v;