--- 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
-