src/HOL/Tools/specification_package.ML

       fun after_qed [[thm]] = ProofContext.theory (fn thy =>
         #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
     in
       thy
       |> ProofContext.init
-      |> Proof.theorem_i PureThy.internalK NONE after_qed
-        (SOME "") ("", []) [(("", []), [(HOLogic.mk_Trueprop ex_prop, [])])]
+      |> Proof.theorem_i PureThy.internalK NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     end;
 
 
 (* outer syntax *)