src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML

--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Wed Mar 04 19:53:18 2015 +0100
@@ -31,7 +31,7 @@
 
 fun string_of_varpow x k =
   let
-    val term = term_of x
+    val term = Thm.term_of x
     val name =
       (case term of
         Free (n, _) => n