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