src/Pure/Proof/proof_syntax.ML

     val thy' = thy
       |> add_proof_syntax
       |> add_proof_atom_consts
         (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names);
   in
-    (Thm.cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
+    (Thm.global_cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
   end;
 
 fun read_term thy topsort =
   let
     val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true));