1.1 --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML Fri Jul 22 07:33:34 2011 +0200
1.2 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML Sat Jul 23 16:12:12 2011 +0200
1.3 @@ -148,9 +148,9 @@
1.4
1.5 (* scanner *)
1.6
1.7 -fun cert_to_pss_tree ctxt input_str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt)
1.8 - (filter_out Symbol.is_blank (Symbol.explode input_str))
1.9 +fun cert_to_pss_tree ctxt input_str =
1.10 + Symbol.scanner "Bad certificate" (parse_cert_tree ctxt)
1.11 + (filter_out Symbol.is_blank (Symbol.explode input_str))
1.12
1.13 end
1.14
1.15 -