# HG changeset patch
# User wenzelm
# Date 1564480315 -7200
# Node ID 56d73e7316c427fc6b2ed2775b0dac9b84d5eac7
# Parent  a21a96eda0332312e5b63cfe49791621efc779cc
clarified context;

diff -r a21a96eda033 -r 56d73e7316c4 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Jul 30 11:41:39 2019 +0200
+++ b/src/Pure/more_thm.ML	Tue Jul 30 11:51:55 2019 +0200
@@ -680,8 +680,9 @@
   let val thm = Thm.transfer' ctxt raw_thm
   in Reconstruct.reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
 
-fun clean_proof_of ctxt full thm =
+fun clean_proof_of ctxt full raw_thm =
   let
+    val thm = Thm.transfer' ctxt raw_thm;
     val (_, prop) =
       Logic.unconstrainT (Thm.shyps_of thm)
         (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
@@ -695,6 +696,7 @@
   end;
 
 
+
 (** forked proofs **)
 
 structure Proofs = Theory_Data