--- 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;