diff -r 286d950883bc -r fe661eb3b0e7 src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Thu Jun 15 18:35:16 2006 +0200
+++ b/src/Pure/Tools/invoke.ML	Thu Jun 15 23:08:54 2006 +0200
@@ -63,7 +63,7 @@
       Seq.map (Proof.map_context (fn ctxt =>
         let
           val ([res_types, res_params, res_prems], ctxt'') =
-            fold_burrow (ProofContext.import false) results ctxt';
+            fold_burrow (Variable.import false) results ctxt';
 
           val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
           val params'' = map (Thm.term_of o Drule.dest_term) res_params;
@@ -99,7 +99,7 @@
 (* FIXME *)
 fun read_terms ctxt args =
   #1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] args)
-  |> ProofContext.polymorphic ctxt;
+  |> Variable.polymorphic ctxt;
 
 (* FIXME *)
 fun cert_terms ctxt args = map fst args;