src/Pure/Proof/proof_syntax.ML

   val term_of_proof: Proofterm.proof -> term
   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
-  val proof_of: theory -> bool -> thm -> Proofterm.proof
+  val proof_of: Proof.context -> bool -> thm -> Proofterm.proof
   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
   val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
 
 structure Proof_Syntax : PROOF_SYNTAX =

     add_proof_syntax #>
     add_proof_atom_consts
       (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
   end;
 
-fun proof_of thy full raw_thm =
-  let
-    val thm = Thm.transfer thy raw_thm;
+fun proof_of ctxt full raw_thm =
+  let
+    val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm;
     val prop = Thm.full_prop_of thm;
     val prf = Thm.proof_of thm;
     val prf' =
       (case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of
         (PThm (_, ((_, prop', _), body)), _) =>
           if prop = prop' then Proofterm.join_proof body else prf
       | _ => prf)
-  in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
+  in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end;
 
 fun pretty_proof ctxt prf =
   Proof_Context.pretty_term_abbrev
     (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
     (term_of_proof prf);
 
 fun pretty_proof_of ctxt full th =
-  pretty_proof ctxt (proof_of (Proof_Context.theory_of ctxt) full th);
+  pretty_proof ctxt (proof_of ctxt full th);
 
 end;