src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
changeset 43946 ba88bb44c192
parent 42361 23f352990944
child 55508 90c42b130652
--- 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
 
-