src/Pure/Tools/invoke.ML

     fun after_qed results =
       Proof.end_block #>
       Seq.map (Proof.map_context (fn ctxt =>
         let
           val ([res_types, res_params, res_prems], ctxt'') =
-            fold_burrow (Variable.import false) results ctxt';
+            fold_burrow (apfst snd oo 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;
           val elems' = elems |> map (Element.inst_ctxt thy
             (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));