src/HOL/Decision_Procs/Approximation.thy

--- a/src/HOL/Decision_Procs/Approximation.thy	Sat Mar 20 02:23:41 2010 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Mar 20 17:33:11 2010 +0100
@@ -3438,7 +3438,7 @@
     | mk_result prec NONE = @{term "UNIV :: real set"}
 
   fun realify t = let
-      val t = Logic.varify t
+      val t = Logic.varify_global t
       val m = map (fn (name, sort) => (name, @{typ real})) (Term.add_tvars t [])
       val t = Term.subst_TVars m t
     in t end