diff -r 1565d476a9e2 -r ed7aa5a350ef src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Tue Apr 03 19:24:11 2007 +0200
+++ b/src/Pure/Tools/invoke.ML	Tue Apr 03 19:24:13 2007 +0200
@@ -63,7 +63,7 @@
       Proof.map_context (fn ctxt =>
         let
           val ([res_types, res_params, res_prems], ctxt'') =
-            fold_burrow (apfst snd oo Variable.import false) results ctxt';
+            fold_burrow (apfst snd oo Variable.import_thms 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;