src/Pure/Tools/invoke.ML

 
           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'')));
+          val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
 
-          val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
           val Element.Notes notes = 
             Element.Notes (maps (Element.facts_of thy) elems')
             |> Element.satisfy_ctxt prems''
             |> Element.map_ctxt_values I I (ProofContext.export ctxt'' ctxt);
-              (* FIXME export typs/terms *)
-
-          val _ = print notes;
-
+            (* FIXME export typs/terms *)
           val notes' = notes
             |> Attrib.map_facts (Attrib.attribute_i thy)
             |> map (fn ((a, atts), facts) => ((a, atts @ more_atts), facts));
-
         in
           ctxt
           |> ProofContext.sticky_prefix prfx
           |> ProofContext.qualified_names
           |> (snd o ProofContext.note_thmss_i notes')
           |> ProofContext.restore_naming ctxt
         end) #> Proof.put_facts NONE);
   in
     state'
-    |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_schematic_i
+    |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i
       "invoke" NONE after_qed propp
     |> Element.refine_witness
     |> Seq.hd
     |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules)))))))
     |> Seq.hd