src/Pure/Proof/proof_syntax.ML

 
 (**** translation between proof terms and pure terms ****)
 
 fun proof_of_term thy ty =
   let
-    val thms = Global_Theory.all_thms_of thy;
+    val thms = Global_Theory.all_thms_of thy true;
     val axms = Theory.all_axioms_of thy;
 
     fun mk_term t = (if ty then I else map_types (K dummyT))
       (Term.no_dummy_patterns t);
 

 
 val term_of_proof = term_of [];
 
 fun cterm_of_proof thy prf =
   let
-    val thm_names = map fst (Global_Theory.all_thms_of thy);
+    val thm_names = map fst (Global_Theory.all_thms_of thy true);
     val axm_names = map fst (Theory.all_axioms_of thy);
     val thy' = thy
       |> add_proof_syntax
       |> add_proof_atom_consts
         (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names);

     (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));
+    val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true));
     val axm_names = map fst (Theory.all_axioms_of thy);
     val ctxt = thy
       |> add_proof_syntax
       |> add_proof_atom_consts
         (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)