# HG changeset patch
# User wenzelm
# Date 1438118080 -7200
# Node ID 695cf1fab6cc5ac1aedfc3781523df4556b53bdf
# Parent  bacfb7c45d8151a1d92506a70b2e414d26dea4ce
clarified context;

diff -r bacfb7c45d81 -r 695cf1fab6cc src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Tue Jul 28 21:47:03 2015 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Tue Jul 28 23:14:40 2015 +0200
@@ -147,7 +147,7 @@
             | _ => AbsP ("H", SOME p, prf)))
           (rec_fns ~~ Thm.prems_of thm)
           (Proofterm.proof_combP
-            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+            (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
 
     val r' =
       if null is then r
@@ -212,10 +212,10 @@
               (AbsP ("H", SOME (Logic.varify_global p), prf)))
           (prems ~~ rs)
           (Proofterm.proof_combP
-            (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+            (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
     val prf' =
       Extraction.abs_corr_shyps thy' exhaust []
-        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
+        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of thy' exhaust);
     val r' =
       Logic.varify_global (Abs ("y", T,
         (fold_rev (Term.abs o dest_Free) rs
diff -r bacfb7c45d81 -r 695cf1fab6cc src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 28 21:47:03 2015 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 28 23:14:40 2015 +0200
@@ -20,7 +20,7 @@
   | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
 
 fun prf_of thy thm =
-  Reconstruct.proof_of thm
+  Reconstruct.proof_of thy thm
   |> Reconstruct.expand_proof thy [("", NONE)];  (* FIXME *)
 
 fun subsets [] = [[]]
diff -r bacfb7c45d81 -r 695cf1fab6cc src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Jul 28 21:47:03 2015 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Jul 28 23:14:40 2015 +0200
@@ -769,9 +769,9 @@
 
       | extr d vs ts Ts hs _ defs = error "extr: bad proof";
 
-    fun prep_thm vs thm =
+    fun prep_thm vs raw_thm =
       let
-        val thy = Thm.theory_of_thm thm;
+        val thm = Thm.transfer thy raw_thm;
         val prop = Thm.prop_of thm;
         val prf = Thm.proof_of thm;
         val name = Thm.derivation_name thm;
diff -r bacfb7c45d81 -r 695cf1fab6cc src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Jul 28 21:47:03 2015 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Jul 28 23:14:40 2015 +0200
@@ -14,7 +14,7 @@
   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: bool -> thm -> Proofterm.proof
+  val proof_of: theory -> bool -> thm -> Proofterm.proof
   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
   val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
@@ -235,9 +235,9 @@
       (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
   end;
 
-fun proof_of full thm =
+fun proof_of thy full raw_thm =
   let
-    val thy = Thm.theory_of_thm thm;
+    val thm = Thm.transfer thy raw_thm;
     val prop = Thm.full_prop_of thm;
     val prf = Thm.proof_of thm;
     val prf' =
@@ -253,6 +253,6 @@
     (term_of_proof prf);
 
 fun pretty_proof_of ctxt full th =
-  pretty_proof ctxt (proof_of full th);
+  pretty_proof ctxt (proof_of (Proof_Context.theory_of ctxt) full th);
 
 end;
diff -r bacfb7c45d81 -r 695cf1fab6cc src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Tue Jul 28 21:47:03 2015 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Tue Jul 28 23:14:40 2015 +0200
@@ -10,7 +10,7 @@
   val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
   val prop_of' : term list -> Proofterm.proof -> term
   val prop_of : Proofterm.proof -> term
-  val proof_of : thm -> Proofterm.proof
+  val proof_of : theory -> thm -> Proofterm.proof
   val expand_proof : theory -> (string * term option) list ->
     Proofterm.proof -> Proofterm.proof
 end;
@@ -324,8 +324,9 @@
 val prop_of' = Envir.beta_eta_contract oo prop_of0;
 val prop_of = prop_of' [];
 
-fun proof_of thm =
-  reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
+fun proof_of thy raw_thm =
+  let val thm = Thm.transfer thy raw_thm
+  in reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm) end;