src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 63201 f151704c08e4
     1.1 --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4  val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
     1.5  
     1.6  fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
     1.7 -  (fn (x, k) => (Proof_Context.cterm_of ctxt (Free (x, @{typ real})), k))
     1.8 +  (fn (x, k) => (Thm.cterm_of ctxt (Free (x, @{typ real})), k))
     1.9  
    1.10  fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
    1.11    (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)