# HG changeset patch
# User wenzelm
# Date 1254422025 -7200
# Node ID d9dfd30af9ae59f52f18c5fd67068c64df14385f
# Parent  3a2fa964ad08d34311ff9b8c5ffa15a3f032da45
core_sos_tac: SUBPROOF body operates on subgoal 1;
tuned;

diff -r 3a2fa964ad08 -r d9dfd30af9ae src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- 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;