# HG changeset patch
# User wenzelm
# Date 1564510165 -7200
# Node ID 6e34025981beaf8337a52fe643c7633791a66a7e
# Parent  bf28f0179914c6e4fdaac6fd0c724e0f9996a056
clarified global theory context;

diff -r bf28f0179914 -r 6e34025981be src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Doc/Implementation/Logic.thy	Tue Jul 30 20:09:25 2019 +0200
@@ -1180,8 +1180,8 @@
   @{index_ML_type proof_body} \\
   @{index_ML Proofterm.proofs: "int Unsynchronized.ref"} \\
   @{index_ML Proofterm.reconstruct_proof:
-  "Proof.context -> term -> proof -> proof"} \\
-  @{index_ML Proofterm.expand_proof: "Proof.context ->
+  "theory -> term -> proof -> proof"} \\
+  @{index_ML Proofterm.expand_proof: "theory ->
   (string * term option) list -> proof -> proof"} \\
   @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
   @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
@@ -1213,7 +1213,7 @@
   additionally records full proof terms. Officially named theorems that
   contribute to a result are recorded in any case.
 
-  \<^descr> \<^ML>\<open>Proofterm.reconstruct_proof\<close>~\<open>ctxt prop prf\<close> turns the implicit
+  \<^descr> \<^ML>\<open>Proofterm.reconstruct_proof\<close>~\<open>thy prop prf\<close> turns the implicit
   proof term \<open>prf\<close> into a full proof of the given proposition.
 
   Reconstruction may fail if \<open>prf\<close> is not a proof of \<open>prop\<close>, or if it does not
@@ -1221,7 +1221,7 @@
   for proofs that are constructed manually, but not for those produced
   automatically by the inference kernel.
 
-  \<^descr> \<^ML>\<open>Proofterm.expand_proof\<close>~\<open>ctxt [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
+  \<^descr> \<^ML>\<open>Proofterm.expand_proof\<close>~\<open>thy [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
   reconstructs the proofs of all specified theorems, with the given (full)
   proof. Theorems that are not unique specified via their name may be
   disambiguated by giving their proposition.
diff -r bf28f0179914 -r 6e34025981be src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/HOL/Extraction.thy	Tue Jul 30 20:09:25 2019 +0200
@@ -16,14 +16,12 @@
   Extraction.add_types
       [("bool", ([], NONE))] #>
   Extraction.set_preprocessor (fn thy =>
-    let val ctxt = Proof_Context.init_global thy in
-      Proofterm.rewrite_proof_notypes
-        ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
-      Proofterm.rewrite_proof thy
-        (RewriteHOLProof.rews,
-         ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class ctxt]) o
-      ProofRewriteRules.elim_vars (curry Const \<^const_name>\<open>default\<close>)
-    end)
+    Proofterm.rewrite_proof_notypes
+      ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
+    Proofterm.rewrite_proof thy
+      (RewriteHOLProof.rews,
+       ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
+    ProofRewriteRules.elim_vars (curry Const \<^const_name>\<open>default\<close>))
 \<close>
 
 lemmas [extraction_expand] =
diff -r bf28f0179914 -r 6e34025981be src/HOL/Proofs/ex/Proof_Terms.thy
--- a/src/HOL/Proofs/ex/Proof_Terms.thy	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Tue Jul 30 20:09:25 2019 +0200
@@ -51,7 +51,6 @@
 
 ML_val \<open>
   val thy = \<^theory>;
-  val ctxt = \<^context>;
   val prf =
     Proof_Syntax.read_proof thy true false
       "impI \<cdot> _ \<cdot> _ \<bullet> \
@@ -59,8 +58,7 @@
       \     conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
       \       (\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
   val thm =
-    prf
-    |> Proofterm.reconstruct_proof ctxt \<^prop>\<open>A \<and> B \<longrightarrow> B \<and> A\<close>
+    Proofterm.reconstruct_proof thy \<^prop>\<open>A \<and> B \<longrightarrow> B \<and> A\<close> prf
     |> Proof_Checker.thm_of_proof thy
     |> Drule.export_without_context;
 \<close>
diff -r bf28f0179914 -r 6e34025981be src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Tue Jul 30 20:09:25 2019 +0200
@@ -12,8 +12,8 @@
 subsection \<open>Export and re-import of global proof terms\<close>
 
 ML \<open>
-  fun export_proof ctxt thm =
-    Proofterm.encode (Thm.clean_proof_of ctxt true thm);
+  fun export_proof thm =
+    Proofterm.encode (Thm.clean_proof_of true thm);
 
   fun import_proof thy xml =
     let
@@ -30,24 +30,24 @@
 lemma ex: "A \<longrightarrow> A" ..
 
 ML_val \<open>
-  val xml = export_proof \<^context> @{thm ex};
+  val xml = export_proof @{thm ex};
   val thm = import_proof thy1 xml;
 \<close>
 
 ML_val \<open>
-  val xml = export_proof \<^context> @{thm de_Morgan};
+  val xml = export_proof @{thm de_Morgan};
   val thm = import_proof thy1 xml;
 \<close>
 
 ML_val \<open>
-  val xml = export_proof \<^context> @{thm Drinker's_Principle};
+  val xml = export_proof @{thm Drinker's_Principle};
   val thm = import_proof thy1 xml;
 \<close>
 
 text \<open>Some fairly large proof:\<close>
 
 ML_val \<open>
-  val xml = export_proof \<^context> @{thm abs_less_iff};
+  val xml = export_proof @{thm abs_less_iff};
   val thm = import_proof thy1 xml;
   \<^assert> (size (YXML.string_of_body xml) > 1000000);
 \<close>
diff -r bf28f0179914 -r 6e34025981be src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Tue Jul 30 20:09:25 2019 +0200
@@ -129,7 +129,6 @@
       |> Global_Theory.store_thm
         (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
       ||> Sign.restore_naming thy;
-    val ctxt' = Proof_Context.init_global thy';
 
     val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
     val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
@@ -148,7 +147,7 @@
             | _ => AbsP ("H", SOME p, prf)))
           (rec_fns ~~ Thm.prems_of thm)
           (Proofterm.proof_combP
-            (Thm.reconstruct_proof_of ctxt' thm', map PBound (length prems - 1 downto 0))));
+            (Thm.reconstruct_proof_of thm', map PBound (length prems - 1 downto 0))));
 
     val r' =
       if null is then r
@@ -204,7 +203,6 @@
       |> Sign.root_path
       |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
       ||> Sign.restore_naming thy;
-    val ctxt' = Proof_Context.init_global thy';
 
     val P = Var (("P", 0), rT' --> HOLogic.boolT);
     val prf =
@@ -214,10 +212,10 @@
               (AbsP ("H", SOME (Logic.varify_global p), prf)))
           (prems ~~ rs)
           (Proofterm.proof_combP
-            (Thm.reconstruct_proof_of ctxt' thm', map PBound (length prems - 1 downto 0))));
+            (Thm.reconstruct_proof_of 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) [])) (Thm.reconstruct_proof_of ctxt' exhaust);
+        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Thm.reconstruct_proof_of exhaust);
     val r' =
       Logic.varify_global (Abs ("y", T,
         (fold_rev (Term.abs o dest_Free) rs
diff -r bf28f0179914 -r 6e34025981be src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 20:09:25 2019 +0200
@@ -19,9 +19,11 @@
     [name] => name
   | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
 
-fun prf_of ctxt thm =
-  Thm.reconstruct_proof_of ctxt thm
-  |> Proofterm.expand_proof ctxt [("", NONE)];  (* FIXME *)
+fun prf_of thy raw_thm =
+  let val thm = Thm.transfer thy raw_thm in
+    Thm.reconstruct_proof_of thm
+    |> Proofterm.expand_proof (Thm.theory_of_thm thm) [("", NONE)]
+  end;
 
 fun subsets [] = [[]]
   | subsets (x::xs) =
@@ -257,7 +259,6 @@
 
 fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
   let
-    val ctxt = Proof_Context.init_global thy;
     val rvs = map fst (relevant_vars (Thm.prop_of rule));
     val xs = rev (Term.add_vars (Thm.prop_of rule) []);
     val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs);
@@ -269,7 +270,7 @@
     if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
     Extraction.abs_corr_shyps thy rule vs vs2
       (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
-         (fold_rev Proofterm.forall_intr_proof' rs (prf_of ctxt rrule)))))
+         (fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule)))))
   end;
 
 fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
diff -r bf28f0179914 -r 6e34025981be src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 30 20:09:25 2019 +0200
@@ -239,12 +239,13 @@
       NONE =>
         let
           val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
+          val thy = Proof_Context.theory_of ctxt;
           val prf = Thm.proof_of thm;
           val prop = Thm.full_prop_of thm;
           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
         in
           Proof_Syntax.pretty_proof ctxt
-            (if full then Proofterm.reconstruct_proof ctxt prop prf' else prf')
+            (if full then Proofterm.reconstruct_proof thy prop prf' else prf')
         end
     | SOME srcs =>
         let
diff -r bf28f0179914 -r 6e34025981be src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Jul 30 20:09:25 2019 +0200
@@ -340,7 +340,7 @@
             (if T = nullT then t else list_comb (t, vars')) $ prop);
       val r = Logic.list_implies (shyps,
         fold_rev Logic.all (map (get_var_type r') vars) r');
-      val prf = Proofterm.reconstruct_proof ctxt' r (rd s2);
+      val prf = Proofterm.reconstruct_proof thy' r (rd s2);
     in (name, (vs, (t, prf))) end
   end;
 
@@ -483,7 +483,6 @@
 fun extract thm_vss thy =
   let
     val thy' = add_syntax thy;
-    val ctxt' = Proof_Context.init_global thy';
 
     val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
       ExtractionData.get thy;
@@ -491,8 +490,8 @@
     val rtypes = map fst types;
     val typroc = typeof_proc [];
     val prep = the_default (K I) prep thy' o
-      ProofRewriteRules.elim_defs ctxt' false (map (Thm.transfer thy) defs) o
-      Proofterm.expand_proof ctxt' (map (rpair NONE) ("" :: expand));
+      ProofRewriteRules.elim_defs thy' false (map (Thm.transfer thy) defs) o
+      Proofterm.expand_proof thy' (map (rpair NONE) ("" :: expand));
     val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
 
     fun find_inst prop Ts ts vs =
@@ -515,7 +514,7 @@
       Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
 
     fun mk_sprfs cs tye = maps (fn (_, T) =>
-      ProofRewriteRules.mk_of_sort_proof ctxt' (map SOME cs)
+      ProofRewriteRules.mk_of_sort_proof thy' (map SOME cs)
         (T, Sign.defaultS thy)) tye;
 
     fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
@@ -616,7 +615,7 @@
                     val _ = msg d ("Building correctness proof for " ^ quote name ^
                       (if null vs' then ""
                        else " (relevant variables: " ^ commas_quote vs' ^ ")"));
-                    val prf' = prep (Proofterm.reconstruct_proof ctxt' prop prf);
+                    val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
                     val (corr_prf0, defs'') = corr (d + 1) vs' [] [] []
                       (rev shyps) NONE prf' prf' defs';
                     val corr_prf = mkabsp shyps corr_prf0;
@@ -640,7 +639,7 @@
             | SOME rs => (case find vs' rs of
                 SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
               | NONE => error ("corr: no realizer for instance of theorem " ^
-                  quote name ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
+                  quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
                     (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
           end
 
@@ -655,7 +654,7 @@
               SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
                 defs)
             | NONE => error ("corr: no realizer for instance of axiom " ^
-                quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
+                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
                   (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))
           end
 
@@ -708,7 +707,7 @@
                     val _ = msg d ("Extracting " ^ quote s ^
                       (if null vs' then ""
                        else " (relevant variables: " ^ commas_quote vs' ^ ")"));
-                    val prf' = prep (Proofterm.reconstruct_proof ctxt' prop prf);
+                    val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
                     val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs;
                     val (corr_prf, defs'') = corr (d + 1) vs' [] [] []
                       (rev shyps) (SOME t) prf' prf' defs';
@@ -756,7 +755,7 @@
             | SOME rs => (case find vs' rs of
                 SOME (t, _) => (subst_TVars tye' t, defs)
               | NONE => error ("extr: no realizer for instance of theorem " ^
-                  quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
+                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
                     (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))
           end
 
@@ -768,7 +767,7 @@
             case find vs' (Symtab.lookup_list realizers s) of
               SOME (t, _) => (subst_TVars tye' t, defs)
             | NONE => error ("extr: no realizer for instance of axiom " ^
-                quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
+                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
                   (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))
           end
 
@@ -783,7 +782,7 @@
         val _ = name <> "" orelse error "extraction: unnamed theorem";
         val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
           quote name ^ " has no computational content")
-      in Proofterm.reconstruct_proof ctxt' prop prf end;
+      in Proofterm.reconstruct_proof thy' prop prf end;
 
     val defs =
       fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)
diff -r bf28f0179914 -r 6e34025981be src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jul 30 20:09:25 2019 +0200
@@ -10,12 +10,12 @@
   val rprocs : bool ->
     (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
   val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
-  val elim_defs : Proof.context -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
+  val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
   val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
   val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
   val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
-  val mk_of_sort_proof : Proof.context -> term option list -> typ * sort -> Proofterm.proof list
-  val expand_of_class : Proof.context -> typ list -> term option list -> Proofterm.proof ->
+  val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
+  val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
     (Proofterm.proof * Proofterm.proof) option
 end;
 
@@ -250,7 +250,7 @@
       | (_, []) => (prf, false)
       | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
 
-fun elim_defs ctxt r defs prf =
+fun elim_defs thy r defs prf =
   let
     val defs' = map (Logic.dest_equals o
       map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
@@ -265,9 +265,9 @@
               then I
               else cons (name, SOME prop)
             | _ => I) [prf] [];
-      in Proofterm.expand_proof ctxt thms end;
+      in Proofterm.expand_proof thy thms end;
   in
-    rewrite_terms (Pattern.rewrite_term (Proof_Context.theory_of ctxt) defs' [])
+    rewrite_terms (Pattern.rewrite_term thy defs' [])
       (fst (insert_refl defnames [] (f prf)))
   end;
 
@@ -340,7 +340,7 @@
 
 (**** expand OfClass proofs ****)
 
-fun mk_of_sort_proof ctxt hs (T, S) =
+fun mk_of_sort_proof thy hs (T, S) =
   let
     val hs' = map
       (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
@@ -354,19 +354,18 @@
         ~1 => error "expand_of_class: missing class hypothesis"
       | i => PBound i;
     fun reconstruct prf prop = prf |>
-      Proofterm.reconstruct_proof ctxt prop |>
-      Proofterm.expand_proof ctxt [("", NONE)] |>
+      Proofterm.reconstruct_proof thy prop |>
+      Proofterm.expand_proof thy [("", NONE)] |>
       Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
   in
     map2 reconstruct
-      (Proofterm.of_sort_proof (Proof_Context.theory_of ctxt)
-        (OfClass o apfst Type.strip_sorts) (subst T, S))
+      (Proofterm.of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
       (Logic.mk_of_sort (T, S))
   end;
 
-fun expand_of_class ctxt Ts hs (OfClass (T, c)) =
-      mk_of_sort_proof ctxt hs (T, [c]) |>
+fun expand_of_class thy Ts hs (OfClass (T, c)) =
+      mk_of_sort_proof thy hs (T, [c]) |>
       hd |> rpair Proofterm.no_skel |> SOME
-  | expand_of_class ctxt Ts hs _ = NONE;
+  | expand_of_class thy Ts hs _ = NONE;
 
 end;
diff -r bf28f0179914 -r 6e34025981be src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Jul 30 20:09:25 2019 +0200
@@ -11,7 +11,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: Proof.context -> bool -> thm -> Proofterm.proof
+  val proof_of: bool -> thm -> Proofterm.proof
   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
   val pretty_clean_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
@@ -177,9 +177,9 @@
       (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
   end;
 
-fun proof_of ctxt full raw_thm =
+fun proof_of full thm =
   let
-    val thm = Thm.transfer' ctxt raw_thm;
+    val thy = Thm.theory_of_thm thm;
     val prop = Thm.full_prop_of thm;
     val prf = Thm.proof_of thm;
     val prf' =
@@ -187,7 +187,7 @@
         (PThm (_, ((_, prop', _, _), body)), _) =>
           if prop = prop' then Proofterm.join_proof body else prf
       | _ => prf)
-  in if full then Proofterm.reconstruct_proof ctxt prop prf' else prf' end;
+  in if full then Proofterm.reconstruct_proof thy prop prf' else prf' end;
 
 fun pretty_proof ctxt prf =
   Proof_Context.pretty_term_abbrev
@@ -195,6 +195,6 @@
     (Proofterm.term_of_proof prf);
 
 fun pretty_clean_proof_of ctxt full thm =
-  pretty_proof ctxt (Thm.clean_proof_of ctxt full thm);
+  pretty_proof ctxt (Thm.clean_proof_of full thm);
 
 end;
diff -r bf28f0179914 -r 6e34025981be src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/more_thm.ML	Tue Jul 30 20:09:25 2019 +0200
@@ -114,8 +114,8 @@
   val tag: string * string -> attribute
   val untag: string -> attribute
   val kind: string -> attribute
-  val reconstruct_proof_of: Proof.context -> thm -> Proofterm.proof
-  val clean_proof_of: Proof.context -> bool -> thm -> Proofterm.proof
+  val reconstruct_proof_of: thm -> Proofterm.proof
+  val clean_proof_of: bool -> thm -> Proofterm.proof
   val register_proofs: thm list lazy -> theory -> theory
   val consolidate_theory: theory -> unit
   val show_consts: bool Config.T
@@ -676,21 +676,20 @@
 
 (** proof terms **)
 
-fun reconstruct_proof_of ctxt raw_thm =
-  let val thm = Thm.transfer' ctxt raw_thm
-  in Proofterm.reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
+fun reconstruct_proof_of thm =
+  Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
 
-fun clean_proof_of ctxt full raw_thm =
+fun clean_proof_of full thm =
   let
-    val thm = Thm.transfer' ctxt raw_thm;
+    val thy = Thm.theory_of_thm thm;
     val (_, prop) =
       Logic.unconstrainT (Thm.shyps_of thm)
         (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
   in
     Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
-    |> Proofterm.reconstruct_proof ctxt prop
-    |> Proofterm.expand_proof ctxt [("", NONE)]
-    |> Proofterm.rew_proof (Proof_Context.theory_of ctxt)
+    |> Proofterm.reconstruct_proof thy prop
+    |> Proofterm.expand_proof thy [("", NONE)]
+    |> Proofterm.rew_proof thy
     |> Proofterm.no_thm_proofs
     |> not full ? Proofterm.shrink_proof
   end;
diff -r bf28f0179914 -r 6e34025981be src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Jul 30 20:09:25 2019 +0200
@@ -152,10 +152,10 @@
     (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
   val rew_proof: theory -> proof -> proof
 
-  val reconstruct_proof: Proof.context -> term -> proof -> proof
+  val reconstruct_proof: theory -> term -> proof -> proof
   val prop_of': term list -> proof -> term
   val prop_of: proof -> term
-  val expand_proof: Proof.context -> (string * term option) list -> proof -> proof
+  val expand_proof: theory -> (string * term option) list -> proof -> proof
 
   val proof_serial: unit -> proof_serial
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
@@ -1629,10 +1629,10 @@
 
 val mk_abs = fold (fn T => fn u => Abs ("", T, u));
 
-fun unifyT ctxt env T U =
+fun unifyT thy env T U =
   let
     val Envir.Envir {maxidx, tenv, tyenv} = env;
-    val (tyenv', maxidx') = Sign.typ_unify (Proof_Context.theory_of ctxt) (T, U) (tyenv, maxidx);
+    val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx);
   in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end;
 
 fun chaseT env (T as TVar v) =
@@ -1641,9 +1641,9 @@
       | SOME T' => chaseT env T')
   | chaseT _ T = T;
 
-fun infer_type ctxt (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs
+fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs
       (t as Const (s, T)) = if T = dummyT then
-        (case Sign.const_type (Proof_Context.theory_of ctxt) s of
+        (case Sign.const_type thy s of
           NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
         | SOME T =>
             let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
@@ -1659,61 +1659,60 @@
         | SOME T => (Free (s, T), T, vTs, env))
       else (t, T, vTs, env)
   | infer_type _ _ _ _ (Var _) = error "reconstruct_proof: internal error"
-  | infer_type ctxt env Ts vTs (Abs (s, T, t)) =
+  | infer_type thy env Ts vTs (Abs (s, T, t)) =
       let
         val (T', env') = if T = dummyT then mk_tvar [] env else (T, env);
-        val (t', U, vTs', env'') = infer_type ctxt env' (T' :: Ts) vTs t
+        val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t
       in (Abs (s, T', t'), T' --> U, vTs', env'') end
-  | infer_type ctxt env Ts vTs (t $ u) =
+  | infer_type thy env Ts vTs (t $ u) =
       let
-        val (t', T, vTs1, env1) = infer_type ctxt env Ts vTs t;
-        val (u', U, vTs2, env2) = infer_type ctxt env1 Ts vTs1 u;
+        val (t', T, vTs1, env1) = infer_type thy env Ts vTs t;
+        val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u;
       in (case chaseT env2 T of
-          Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT ctxt env2 U U')
+          Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U')
         | _ =>
           let val (V, env3) = mk_tvar [] env2
-          in (t' $ u', V, vTs2, unifyT ctxt env3 T (U --> V)) end)
+          in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end)
       end
   | infer_type _ env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env)
       handle General.Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
 
-fun cantunify ctxt (t, u) =
+fun cantunify thy (t, u) =
   error ("Non-unifiable terms:\n" ^
-    Syntax.string_of_term ctxt t ^ "\n\n" ^ Syntax.string_of_term ctxt u);
+    Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u);
 
-fun decompose ctxt Ts (p as (t, u)) env =
+fun decompose thy Ts (p as (t, u)) env =
   let
     fun rigrig (a, T) (b, U) uT ts us =
-      if a <> b then cantunify ctxt p
-      else apfst flat (fold_map (decompose ctxt Ts) (ts ~~ us) (uT env T U))
+      if a <> b then cantunify thy p
+      else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U))
   in
     case apply2 (strip_comb o Envir.head_norm env) p of
-      ((Const c, ts), (Const d, us)) => rigrig c d (unifyT ctxt) ts us
-    | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT ctxt) ts us
+      ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us
+    | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us
     | ((Bound i, ts), (Bound j, us)) =>
         rigrig (i, dummyT) (j, dummyT) (K o K) ts us
     | ((Abs (_, T, t), []), (Abs (_, U, u), [])) =>
-        decompose ctxt (T::Ts) (t, u) (unifyT ctxt env T U)
+        decompose thy (T::Ts) (t, u) (unifyT thy env T U)
     | ((Abs (_, T, t), []), _) =>
-        decompose ctxt (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env
+        decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env
     | (_, (Abs (_, T, u), [])) =>
-        decompose ctxt (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env
+        decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env
     | _ => ([(mk_abs Ts t, mk_abs Ts u)], env)
   end;
 
-fun make_constraints_cprf ctxt env cprf =
+fun make_constraints_cprf thy env cprf =
   let
     fun add_cnstrt Ts prop prf cs env vTs (t, u) =
       let
         val t' = mk_abs Ts t;
         val u' = mk_abs Ts u
       in
-        (prop, prf, cs, Pattern.unify (Context.Proof ctxt) (t', u') env, vTs)
-        handle Pattern.Pattern =>
-            let val (cs', env') = decompose ctxt [] (t', u') env
+        (prop, prf, cs, Pattern.unify (Context.Theory thy) (t', u') env, vTs)
+          handle Pattern.Pattern =>
+            let val (cs', env') = decompose thy [] (t', u') env
             in (prop, prf, cs @ cs', env', vTs) end
-        | Pattern.Unif =>
-            cantunify ctxt (Envir.norm_term env t', Envir.norm_term env u')
+          | Pattern.Unif => cantunify thy (Envir.norm_term env t', Envir.norm_term env u')
       end;
 
     fun mk_cnstrts_atom env vTs prop opTs prf =
@@ -1748,7 +1747,7 @@
           end
       | mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) =
           let
-            val (t', _, vTs', env') = infer_type ctxt env Ts vTs t;
+            val (t', _, vTs', env') = infer_type thy env Ts vTs t;
             val (u, prf, cnstrts, env'', vTs'') = mk_cnstrts env' Ts (t'::Hs) vTs' cprf;
           in (Logic.mk_implies (t', u), AbsP (s, SOME t', prf), cnstrts, env'', vTs'')
           end
@@ -1771,11 +1770,11 @@
                 end)
           end
       | mk_cnstrts env Ts Hs vTs (cprf % SOME t) =
-          let val (t', U, vTs1, env1) = infer_type ctxt env Ts vTs t
+          let val (t', U, vTs1, env1) = infer_type thy env Ts vTs t
           in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of
              (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
                  prf, cnstrts, env2, vTs2) =>
-               let val env3 = unifyT ctxt env2 T U
+               let val env3 = unifyT thy env2 T U
                in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2)
                end
            | (u, prf, cnstrts, env2, vTs2) =>
@@ -1838,11 +1837,13 @@
 (* solution of constraints *)
 
 fun solve _ [] bigenv = bigenv
-  | solve ctxt cs bigenv =
+  | solve thy cs bigenv =
       let
-        fun search _ [] = error ("Unsolvable constraints:\n" ^
-              Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
-                Syntax.pretty_flexpair ctxt (apply2 (Envir.norm_term bigenv) p)) cs)))
+        fun search _ [] =
+              error ("Unsolvable constraints:\n" ^
+                Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
+                  Syntax.pretty_flexpair (Syntax.init_pretty_global thy)
+                    (apply2 (Envir.norm_term bigenv) p)) cs)))
           | search env ((u, p as (t1, t2), vs)::ps) =
               if u then
                 let
@@ -1850,10 +1851,10 @@
                   val tn2 = Envir.norm_term bigenv t2
                 in
                   if Pattern.pattern tn1 andalso Pattern.pattern tn2 then
-                    (Pattern.unify (Context.Proof ctxt) (tn1, tn2) env, ps) handle Pattern.Unif =>
-                       cantunify ctxt (tn1, tn2)
+                    (Pattern.unify (Context.Theory thy) (tn1, tn2) env, ps)
+                      handle Pattern.Unif => cantunify thy (tn1, tn2)
                   else
-                    let val (cs', env') = decompose ctxt [] (tn1, tn2) env
+                    let val (cs', env') = decompose thy [] (tn1, tn2) env
                     in if cs' = [(tn1, tn2)] then
                          apsnd (cons (false, (tn1, tn2), vs)) (search env ps)
                        else search env' (map (fn q => (true, q, vs)) cs' @ ps)
@@ -1863,7 +1864,7 @@
         val Envir.Envir {maxidx, ...} = bigenv;
         val (env, cs') = search (Envir.empty maxidx) cs;
       in
-        solve ctxt (upd_constrs env cs') (Envir.merge (bigenv, env))
+        solve thy (upd_constrs env cs') (Envir.merge (bigenv, env))
       end;
 
 in
@@ -1871,18 +1872,16 @@
 
 (* reconstruction of proofs *)
 
-fun reconstruct_proof ctxt prop cprf =
+fun reconstruct_proof thy prop cprf =
   let
     val (cprf' % SOME prop', thawf) = freeze_thaw_prf (cprf % SOME prop);
-    val (t, prf, cs, env, _) = make_constraints_cprf ctxt
+    val (t, prf, cs, env, _) = make_constraints_cprf thy
       (Envir.empty (maxidx_proof cprf ~1)) cprf';
     val cs' =
       map (apply2 (Envir.norm_term env)) ((t, prop') :: cs)
       |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) [])));
-    val env' = solve ctxt cs' env
-  in
-    thawf (norm_proof env' prf)
-  end;
+    val env' = solve thy cs' env
+  in thawf (norm_proof env' prf) end;
 
 fun prop_of_atom prop Ts = subst_atomic_types
   (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
@@ -1914,7 +1913,7 @@
 
 (* expand and reconstruct subproofs *)
 
-fun expand_proof ctxt thms prf =
+fun expand_proof thy thms prf =
   let
     fun expand maxidx prfs (AbsP (s, t, prf)) =
           let val (maxidx', prfs', prf') = expand maxidx prfs prf
@@ -1943,7 +1942,7 @@
                     val prf' =
                       join_proof body
                       |> open_proof
-                      |> reconstruct_proof ctxt prop
+                      |> reconstruct_proof thy prop
                       |> forall_intr_vfs_prf prop;
                     val (maxidx', prfs', prf) = expand (maxidx_proof prf' ~1) prfs prf'
                   in
@@ -2020,10 +2019,9 @@
 fun export thy i prop proof =
   if Options.default_bool "export_proofs" then
     let
-      val thy_ctxt = Proof_Context.init_global thy;
       val xml =
-        reconstruct_proof thy_ctxt prop proof
-        |> expand_proof thy_ctxt [("", NONE)]
+        reconstruct_proof thy prop proof
+        |> expand_proof thy [("", NONE)]
         |> term_of_proof
         |> Term_XML.Encode.term;
     in