tuned;
authorwenzelm
Sat, 23 Jul 2011 16:12:12 +0200
changeset 44817ba88bb44c192
parent 44816 48065e997df0
child 44818 9b00f09f7721
tuned;
src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
     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 -