# HG changeset patch
# User wenzelm
# Date 1563786564 -7200
# Node ID 772321761cb8516ef1033b47f3b3e90b5fa49b17
# Parent  2adff54de67eb4adf58652b6d5dad5010d6ca610
unused (see also 42fbb6abed5a);

diff -r 2adff54de67e -r 772321761cb8 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Sun Jul 21 15:42:43 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Mon Jul 22 11:09:24 2019 +0200
@@ -8,7 +8,6 @@
 sig
   val add_proof_syntax: theory -> theory
   val proof_of_term: theory -> bool -> term -> Proofterm.proof
-  val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
   val read_term: theory -> bool -> typ -> string -> term
   val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
   val proof_syntax: Proofterm.proof -> theory -> theory
@@ -140,18 +139,6 @@
   in prf_of [] end;
 
 
-fun cterm_of_proof thy prf =
-  let
-    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);
-  in
-    (Thm.global_cterm_of thy' (Proofterm.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));