src/Pure/Isar/specification.ML

             else #2 (LocalTheory.notes [((name, atts), [(maps #2 res, [])])] lthy')))
         |> after_qed results'
       end;
   in
     goal_ctxt
-    |> Proof.global_goal (K (K ())) Attrib.attribute_i ProofContext.bind_propp_schematic_i
-      kind before_qed after_qed' NONE (name, []) stmt
+    |> Proof.theorem_i kind before_qed after_qed' (map snd stmt)
     |> Proof.refine_insert facts
   end;
 
 in