src/Pure/tctical.ML

--- a/src/Pure/tctical.ML	Tue Jul 25 21:17:58 2006 +0200
+++ b/src/Pure/tctical.ML	Tue Jul 25 21:18:00 2006 +0200
@@ -375,7 +375,7 @@
 fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) =
         strip_context_aux (params, H::Hs, B)
   | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) =
-        let val (b,u) = variant_abs(a,T,t)
+        let val (b,u) = Syntax.variant_abs(a,T,t)
         in  strip_context_aux ((b,T)::params, Hs, u)  end
   | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);