# HG changeset patch
# User wenzelm
# Date 1311430332 -7200
# Node ID ba88bb44c19282b9ab4d3b3cfe4651372c0b66bc
# Parent  48065e997df03a62b9a1b74c2534cfd2b57d8aaf
tuned;

diff -r 48065e997df0 -r ba88bb44c192 src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Fri Jul 22 07:33:34 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Sat Jul 23 16:12:12 2011 +0200
@@ -148,9 +148,9 @@
 
 (* scanner *)
 
-fun cert_to_pss_tree ctxt input_str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt)
-  (filter_out Symbol.is_blank (Symbol.explode input_str))
+fun cert_to_pss_tree ctxt input_str =
+  Symbol.scanner "Bad certificate" (parse_cert_tree ctxt)
+    (filter_out Symbol.is_blank (Symbol.explode input_str))
 
 end
 
-