clarified context;
authorwenzelm
Sat Apr 09 13:28:32 2016 +0200 (2016-04-09 ago)
changeset 6292296691631c1eb
parent 62921 499a63c30d55
child 62923 3a122e1e352a
clarified context;
avoid Unsynchronized.ref;
src/Doc/Implementation/Logic.thy
src/HOL/Extraction.thy
src/HOL/Proofs/ex/Proof_Terms.thy
src/HOL/Proofs/ex/XML_Data.thy
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/inductive_realizer.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
     1.1 --- a/src/Doc/Implementation/Logic.thy	Sat Apr 09 12:36:25 2016 +0200
     1.2 +++ b/src/Doc/Implementation/Logic.thy	Sat Apr 09 13:28:32 2016 +0200
     1.3 @@ -1188,8 +1188,8 @@
     1.4    @{index_ML_type proof_body} \\
     1.5    @{index_ML proofs: "int Unsynchronized.ref"} \\
     1.6    @{index_ML Reconstruct.reconstruct_proof:
     1.7 -  "theory -> term -> proof -> proof"} \\
     1.8 -  @{index_ML Reconstruct.expand_proof: "theory ->
     1.9 +  "Proof.context -> term -> proof -> proof"} \\
    1.10 +  @{index_ML Reconstruct.expand_proof: "Proof.context ->
    1.11    (string * term option) list -> proof -> proof"} \\
    1.12    @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
    1.13    @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
    1.14 @@ -1221,7 +1221,7 @@
    1.15    records full proof terms. Officially named theorems that contribute to a
    1.16    result are recorded in any case.
    1.17  
    1.18 -  \<^descr> @{ML Reconstruct.reconstruct_proof}~\<open>thy prop prf\<close> turns the implicit
    1.19 +  \<^descr> @{ML Reconstruct.reconstruct_proof}~\<open>ctxt prop prf\<close> turns the implicit
    1.20    proof term \<open>prf\<close> into a full proof of the given proposition.
    1.21  
    1.22    Reconstruction may fail if \<open>prf\<close> is not a proof of \<open>prop\<close>, or if it does not
    1.23 @@ -1229,7 +1229,7 @@
    1.24    for proofs that are constructed manually, but not for those produced
    1.25    automatically by the inference kernel.
    1.26  
    1.27 -  \<^descr> @{ML Reconstruct.expand_proof}~\<open>thy [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
    1.28 +  \<^descr> @{ML Reconstruct.expand_proof}~\<open>ctxt [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
    1.29    reconstructs the proofs of all specified theorems, with the given (full)
    1.30    proof. Theorems that are not unique specified via their name may be
    1.31    disambiguated by giving their proposition.
     2.1 --- a/src/HOL/Extraction.thy	Sat Apr 09 12:36:25 2016 +0200
     2.2 +++ b/src/HOL/Extraction.thy	Sat Apr 09 13:28:32 2016 +0200
     2.3 @@ -16,12 +16,14 @@
     2.4    Extraction.add_types
     2.5        [("bool", ([], NONE))] #>
     2.6    Extraction.set_preprocessor (fn thy =>
     2.7 +    let val ctxt = Proof_Context.init_global thy in
     2.8        Proofterm.rewrite_proof_notypes
     2.9          ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
    2.10        Proofterm.rewrite_proof thy
    2.11          (RewriteHOLProof.rews,
    2.12 -         ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
    2.13 -      ProofRewriteRules.elim_vars (curry Const @{const_name default}))
    2.14 +         ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class ctxt]) o
    2.15 +      ProofRewriteRules.elim_vars (curry Const @{const_name default})
    2.16 +    end)
    2.17  \<close>
    2.18  
    2.19  lemmas [extraction_expand] =
     3.1 --- a/src/HOL/Proofs/ex/Proof_Terms.thy	Sat Apr 09 12:36:25 2016 +0200
     3.2 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Sat Apr 09 13:28:32 2016 +0200
     3.3 @@ -46,6 +46,7 @@
     3.4  
     3.5  ML_val \<open>
     3.6    val thy = @{theory};
     3.7 +  val ctxt = @{context};
     3.8    val prf =
     3.9      Proof_Syntax.read_proof thy true false
    3.10        "impI \<cdot> _ \<cdot> _ \<bullet> \
    3.11 @@ -54,7 +55,7 @@
    3.12        \       (\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
    3.13    val thm =
    3.14      prf
    3.15 -    |> Reconstruct.reconstruct_proof thy @{prop "A \<and> B \<longrightarrow> B \<and> A"}
    3.16 +    |> Reconstruct.reconstruct_proof ctxt @{prop "A \<and> B \<longrightarrow> B \<and> A"}
    3.17      |> Proof_Checker.thm_of_proof thy
    3.18      |> Drule.export_without_context;
    3.19  \<close>
     4.1 --- a/src/HOL/Proofs/ex/XML_Data.thy	Sat Apr 09 12:36:25 2016 +0200
     4.2 +++ b/src/HOL/Proofs/ex/XML_Data.thy	Sat Apr 09 13:28:32 2016 +0200
     4.3 @@ -12,15 +12,16 @@
     4.4  subsection \<open>Export and re-import of global proof terms\<close>
     4.5  
     4.6  ML \<open>
     4.7 -  fun export_proof thy thm =
     4.8 +  fun export_proof ctxt thm =
     4.9      let
    4.10 +      val thy = Proof_Context.theory_of ctxt;
    4.11        val (_, prop) =
    4.12          Logic.unconstrainT (Thm.shyps_of thm)
    4.13            (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
    4.14        val prf =
    4.15          Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |>
    4.16 -        Reconstruct.reconstruct_proof thy prop |>
    4.17 -        Reconstruct.expand_proof thy [("", NONE)] |>
    4.18 +        Reconstruct.reconstruct_proof ctxt prop |>
    4.19 +        Reconstruct.expand_proof ctxt [("", NONE)] |>
    4.20          Proofterm.rew_proof thy |>
    4.21          Proofterm.no_thm_proofs;
    4.22      in Proofterm.encode prf end;
    4.23 @@ -40,24 +41,24 @@
    4.24  lemma ex: "A \<longrightarrow> A" ..
    4.25  
    4.26  ML_val \<open>
    4.27 -  val xml = export_proof @{theory} @{thm ex};
    4.28 +  val xml = export_proof @{context} @{thm ex};
    4.29    val thm = import_proof thy1 xml;
    4.30  \<close>
    4.31  
    4.32  ML_val \<open>
    4.33 -  val xml = export_proof @{theory} @{thm de_Morgan};
    4.34 +  val xml = export_proof @{context} @{thm de_Morgan};
    4.35    val thm = import_proof thy1 xml;
    4.36  \<close>
    4.37  
    4.38  ML_val \<open>
    4.39 -  val xml = export_proof @{theory} @{thm Drinker's_Principle};
    4.40 +  val xml = export_proof @{context} @{thm Drinker's_Principle};
    4.41    val thm = import_proof thy1 xml;
    4.42  \<close>
    4.43  
    4.44  text \<open>Some fairly large proof:\<close>
    4.45  
    4.46  ML_val \<open>
    4.47 -  val xml = export_proof @{theory} @{thm abs_less_iff};
    4.48 +  val xml = export_proof @{context} @{thm abs_less_iff};
    4.49    val thm = import_proof thy1 xml;
    4.50    @{assert} (size (YXML.string_of_body xml) > 1000000);
    4.51  \<close>
     5.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sat Apr 09 12:36:25 2016 +0200
     5.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sat Apr 09 13:28:32 2016 +0200
     5.3 @@ -129,6 +129,7 @@
     5.4        |> Global_Theory.store_thm
     5.5          (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
     5.6        ||> Sign.restore_naming thy;
     5.7 +    val ctxt' = Proof_Context.init_global thy';
     5.8  
     5.9      val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
    5.10      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
    5.11 @@ -147,7 +148,7 @@
    5.12              | _ => AbsP ("H", SOME p, prf)))
    5.13            (rec_fns ~~ Thm.prems_of thm)
    5.14            (Proofterm.proof_combP
    5.15 -            (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
    5.16 +            (Reconstruct.proof_of ctxt' thm', map PBound (length prems - 1 downto 0))));
    5.17  
    5.18      val r' =
    5.19        if null is then r
    5.20 @@ -203,6 +204,7 @@
    5.21        |> Sign.root_path
    5.22        |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
    5.23        ||> Sign.restore_naming thy;
    5.24 +    val ctxt' = Proof_Context.init_global thy';
    5.25  
    5.26      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    5.27      val prf =
    5.28 @@ -212,10 +214,10 @@
    5.29                (AbsP ("H", SOME (Logic.varify_global p), prf)))
    5.30            (prems ~~ rs)
    5.31            (Proofterm.proof_combP
    5.32 -            (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
    5.33 +            (Reconstruct.proof_of ctxt' thm', map PBound (length prems - 1 downto 0))));
    5.34      val prf' =
    5.35        Extraction.abs_corr_shyps thy' exhaust []
    5.36 -        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of thy' exhaust);
    5.37 +        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of ctxt' exhaust);
    5.38      val r' =
    5.39        Logic.varify_global (Abs ("y", T,
    5.40          (fold_rev (Term.abs o dest_Free) rs
     6.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Apr 09 12:36:25 2016 +0200
     6.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Apr 09 13:28:32 2016 +0200
     6.3 @@ -19,9 +19,9 @@
     6.4      [name] => name
     6.5    | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
     6.6  
     6.7 -fun prf_of thy thm =
     6.8 -  Reconstruct.proof_of thy thm
     6.9 -  |> Reconstruct.expand_proof thy [("", NONE)];  (* FIXME *)
    6.10 +fun prf_of ctxt thm =
    6.11 +  Reconstruct.proof_of ctxt thm
    6.12 +  |> Reconstruct.expand_proof ctxt [("", NONE)];  (* FIXME *)
    6.13  
    6.14  fun subsets [] = [[]]
    6.15    | subsets (x::xs) =
    6.16 @@ -257,6 +257,7 @@
    6.17  
    6.18  fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
    6.19    let
    6.20 +    val ctxt = Proof_Context.init_global thy;
    6.21      val rvs = map fst (relevant_vars (Thm.prop_of rule));
    6.22      val xs = rev (Term.add_vars (Thm.prop_of rule) []);
    6.23      val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs);
    6.24 @@ -268,7 +269,7 @@
    6.25      if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
    6.26      Extraction.abs_corr_shyps thy rule vs vs2
    6.27        (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
    6.28 -         (fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule)))))
    6.29 +         (fold_rev Proofterm.forall_intr_proof' rs (prf_of ctxt rrule)))))
    6.30    end;
    6.31  
    6.32  fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
     7.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Apr 09 12:36:25 2016 +0200
     7.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 09 13:28:32 2016 +0200
     7.3 @@ -250,13 +250,12 @@
     7.4        NONE =>
     7.5          let
     7.6            val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
     7.7 -          val thy = Proof_Context.theory_of ctxt;
     7.8            val prf = Thm.proof_of thm;
     7.9            val prop = Thm.full_prop_of thm;
    7.10            val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
    7.11          in
    7.12            Proof_Syntax.pretty_proof ctxt
    7.13 -            (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
    7.14 +            (if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf')
    7.15          end
    7.16      | SOME srcs =>
    7.17          let val ctxt = Toplevel.context_of state
     8.1 --- a/src/Pure/Proof/extraction.ML	Sat Apr 09 12:36:25 2016 +0200
     8.2 +++ b/src/Pure/Proof/extraction.ML	Sat Apr 09 13:28:32 2016 +0200
     8.3 @@ -164,13 +164,13 @@
     8.4      | _ => error "get_var_type: not a variable"
     8.5    end;
     8.6  
     8.7 -fun read_term thy T s =
     8.8 +fun read_term ctxt T s =
     8.9    let
    8.10 -    val ctxt = Proof_Context.init_global thy
    8.11 +    val ctxt' = ctxt
    8.12        |> Config.put Type_Infer_Context.const_sorts false
    8.13        |> Proof_Context.set_defsort [];
    8.14      val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
    8.15 -  in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
    8.16 +  in parse ctxt' s |> Type.constraint T |> Syntax.check_term ctxt' end;
    8.17  
    8.18  
    8.19  (**** theory data ****)
    8.20 @@ -214,9 +214,9 @@
    8.21  );
    8.22  
    8.23  fun read_condeq thy =
    8.24 -  let val thy' = add_syntax thy
    8.25 +  let val ctxt' = Proof_Context.init_global (add_syntax thy)
    8.26    in fn s =>
    8.27 -    let val t = Logic.varify_global (read_term thy' propT s)
    8.28 +    let val t = Logic.varify_global (read_term ctxt' propT s)
    8.29      in
    8.30        (map Logic.dest_equals (Logic.strip_imp_prems t),
    8.31          Logic.dest_equals (Logic.strip_imp_concl t))
    8.32 @@ -314,6 +314,7 @@
    8.33      val rtypes = map fst types;
    8.34      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    8.35      val thy' = add_syntax thy;
    8.36 +    val ctxt' = Proof_Context.init_global thy';
    8.37      val rd = Proof_Syntax.read_proof thy' true false;
    8.38    in fn (thm, (vs, s1, s2)) =>
    8.39      let
    8.40 @@ -331,14 +332,14 @@
    8.41        val T = etype_of thy' vs [] prop;
    8.42        val (T', thw) = Type.legacy_freeze_thaw_type
    8.43          (if T = nullT then nullT else map fastype_of vars' ---> T);
    8.44 -      val t = map_types thw (read_term thy' T' s1);
    8.45 +      val t = map_types thw (read_term ctxt' T' s1);
    8.46        val r' = freeze_thaw (condrew thy' eqns
    8.47          (procs @ [typeof_proc [] vs, rlz_proc]))
    8.48            (Const ("realizes", T --> propT --> propT) $
    8.49              (if T = nullT then t else list_comb (t, vars')) $ prop);
    8.50        val r = Logic.list_implies (shyps,
    8.51          fold_rev Logic.all (map (get_var_type r') vars) r');
    8.52 -      val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
    8.53 +      val prf = Reconstruct.reconstruct_proof ctxt' r (rd s2);
    8.54      in (name, (vs, (t, prf))) end
    8.55    end;
    8.56  
    8.57 @@ -481,14 +482,16 @@
    8.58  fun extract thm_vss thy =
    8.59    let
    8.60      val thy' = add_syntax thy;
    8.61 +    val ctxt' = Proof_Context.init_global thy';
    8.62 +
    8.63      val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
    8.64        ExtractionData.get thy;
    8.65      val procs = maps (rev o fst o snd) types;
    8.66      val rtypes = map fst types;
    8.67      val typroc = typeof_proc [];
    8.68      val prep = the_default (K I) prep thy' o
    8.69 -      ProofRewriteRules.elim_defs thy' false (map (Thm.transfer thy) defs) o
    8.70 -      Reconstruct.expand_proof thy' (map (rpair NONE) ("" :: expand));
    8.71 +      ProofRewriteRules.elim_defs ctxt' false (map (Thm.transfer thy) defs) o
    8.72 +      Reconstruct.expand_proof ctxt' (map (rpair NONE) ("" :: expand));
    8.73      val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    8.74  
    8.75      fun find_inst prop Ts ts vs =
    8.76 @@ -511,7 +514,7 @@
    8.77        Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
    8.78  
    8.79      fun mk_sprfs cs tye = maps (fn (_, T) =>
    8.80 -      ProofRewriteRules.mk_of_sort_proof thy (map SOME cs)
    8.81 +      ProofRewriteRules.mk_of_sort_proof ctxt' (map SOME cs)
    8.82          (T, Sign.defaultS thy)) tye;
    8.83  
    8.84      fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
    8.85 @@ -612,7 +615,7 @@
    8.86                      val _ = msg d ("Building correctness proof for " ^ quote name ^
    8.87                        (if null vs' then ""
    8.88                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
    8.89 -                    val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
    8.90 +                    val prf' = prep (Reconstruct.reconstruct_proof ctxt' prop prf);
    8.91                      val (corr_prf0, defs'') = corr (d + 1) vs' [] [] []
    8.92                        (rev shyps) NONE prf' prf' defs';
    8.93                      val corr_prf = mkabsp shyps corr_prf0;
    8.94 @@ -636,7 +639,7 @@
    8.95              | SOME rs => (case find vs' rs of
    8.96                  SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
    8.97                | NONE => error ("corr: no realizer for instance of theorem " ^
    8.98 -                  quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
    8.99 +                  quote name ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
   8.100                      (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))))
   8.101            end
   8.102  
   8.103 @@ -651,7 +654,7 @@
   8.104                SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
   8.105                  defs)
   8.106              | NONE => error ("corr: no realizer for instance of axiom " ^
   8.107 -                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   8.108 +                quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
   8.109                    (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
   8.110            end
   8.111  
   8.112 @@ -704,7 +707,7 @@
   8.113                      val _ = msg d ("Extracting " ^ quote s ^
   8.114                        (if null vs' then ""
   8.115                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   8.116 -                    val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   8.117 +                    val prf' = prep (Reconstruct.reconstruct_proof ctxt' prop prf);
   8.118                      val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs;
   8.119                      val (corr_prf, defs'') = corr (d + 1) vs' [] [] []
   8.120                        (rev shyps) (SOME t) prf' prf' defs';
   8.121 @@ -752,7 +755,7 @@
   8.122              | SOME rs => (case find vs' rs of
   8.123                  SOME (t, _) => (subst_TVars tye' t, defs)
   8.124                | NONE => error ("extr: no realizer for instance of theorem " ^
   8.125 -                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   8.126 +                  quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
   8.127                      (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
   8.128            end
   8.129  
   8.130 @@ -764,7 +767,7 @@
   8.131              case find vs' (Symtab.lookup_list realizers s) of
   8.132                SOME (t, _) => (subst_TVars tye' t, defs)
   8.133              | NONE => error ("extr: no realizer for instance of axiom " ^
   8.134 -                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   8.135 +                quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
   8.136                    (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
   8.137            end
   8.138  
   8.139 @@ -779,7 +782,7 @@
   8.140          val _ = name <> "" orelse error "extraction: unnamed theorem";
   8.141          val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
   8.142            quote name ^ " has no computational content")
   8.143 -      in Reconstruct.reconstruct_proof thy prop prf end;
   8.144 +      in Reconstruct.reconstruct_proof ctxt' prop prf end;
   8.145  
   8.146      val defs =
   8.147        fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)
     9.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat Apr 09 12:36:25 2016 +0200
     9.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat Apr 09 13:28:32 2016 +0200
     9.3 @@ -10,12 +10,12 @@
     9.4    val rprocs : bool ->
     9.5      (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
     9.6    val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
     9.7 -  val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
     9.8 +  val elim_defs : Proof.context -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
     9.9    val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
    9.10    val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
    9.11    val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
    9.12 -  val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
    9.13 -  val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
    9.14 +  val mk_of_sort_proof : Proof.context -> term option list -> typ * sort -> Proofterm.proof list
    9.15 +  val expand_of_class : Proof.context -> typ list -> term option list -> Proofterm.proof ->
    9.16      (Proofterm.proof * Proofterm.proof) option
    9.17  end;
    9.18  
    9.19 @@ -250,7 +250,7 @@
    9.20        | (_, []) => (prf, false)
    9.21        | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
    9.22  
    9.23 -fun elim_defs thy r defs prf =
    9.24 +fun elim_defs ctxt r defs prf =
    9.25    let
    9.26      val defs' = map (Logic.dest_equals o
    9.27        map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
    9.28 @@ -265,9 +265,9 @@
    9.29                then I
    9.30                else cons (name, SOME prop)
    9.31              | _ => I) [prf] [];
    9.32 -      in Reconstruct.expand_proof thy thms end;
    9.33 +      in Reconstruct.expand_proof ctxt thms end;
    9.34    in
    9.35 -    rewrite_terms (Pattern.rewrite_term thy defs' [])
    9.36 +    rewrite_terms (Pattern.rewrite_term (Proof_Context.theory_of ctxt) defs' [])
    9.37        (fst (insert_refl defnames [] (f prf)))
    9.38    end;
    9.39  
    9.40 @@ -340,7 +340,7 @@
    9.41  
    9.42  (**** expand OfClass proofs ****)
    9.43  
    9.44 -fun mk_of_sort_proof thy hs (T, S) =
    9.45 +fun mk_of_sort_proof ctxt hs (T, S) =
    9.46    let
    9.47      val hs' = map
    9.48        (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
    9.49 @@ -354,18 +354,19 @@
    9.50          ~1 => error "expand_of_class: missing class hypothesis"
    9.51        | i => PBound i;
    9.52      fun reconstruct prf prop = prf |>
    9.53 -      Reconstruct.reconstruct_proof thy prop |>
    9.54 -      Reconstruct.expand_proof thy [("", NONE)] |>
    9.55 +      Reconstruct.reconstruct_proof ctxt prop |>
    9.56 +      Reconstruct.expand_proof ctxt [("", NONE)] |>
    9.57        Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
    9.58    in
    9.59      map2 reconstruct
    9.60 -      (Proofterm.of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
    9.61 +      (Proofterm.of_sort_proof (Proof_Context.theory_of ctxt)
    9.62 +        (OfClass o apfst Type.strip_sorts) (subst T, S))
    9.63        (Logic.mk_of_sort (T, S))
    9.64    end;
    9.65  
    9.66 -fun expand_of_class thy Ts hs (OfClass (T, c)) =
    9.67 -      mk_of_sort_proof thy hs (T, [c]) |>
    9.68 +fun expand_of_class ctxt Ts hs (OfClass (T, c)) =
    9.69 +      mk_of_sort_proof ctxt hs (T, [c]) |>
    9.70        hd |> rpair Proofterm.no_skel |> SOME
    9.71 -  | expand_of_class thy Ts hs _ = NONE;
    9.72 +  | expand_of_class ctxt Ts hs _ = NONE;
    9.73  
    9.74  end;
    10.1 --- a/src/Pure/Proof/proof_syntax.ML	Sat Apr 09 12:36:25 2016 +0200
    10.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sat Apr 09 13:28:32 2016 +0200
    10.3 @@ -14,7 +14,7 @@
    10.4    val read_term: theory -> bool -> typ -> string -> term
    10.5    val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
    10.6    val proof_syntax: Proofterm.proof -> theory -> theory
    10.7 -  val proof_of: theory -> bool -> thm -> Proofterm.proof
    10.8 +  val proof_of: Proof.context -> bool -> thm -> Proofterm.proof
    10.9    val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
   10.10    val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
   10.11  end;
   10.12 @@ -239,9 +239,9 @@
   10.13        (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
   10.14    end;
   10.15  
   10.16 -fun proof_of thy full raw_thm =
   10.17 +fun proof_of ctxt full raw_thm =
   10.18    let
   10.19 -    val thm = Thm.transfer thy raw_thm;
   10.20 +    val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm;
   10.21      val prop = Thm.full_prop_of thm;
   10.22      val prf = Thm.proof_of thm;
   10.23      val prf' =
   10.24 @@ -249,7 +249,7 @@
   10.25          (PThm (_, ((_, prop', _), body)), _) =>
   10.26            if prop = prop' then Proofterm.join_proof body else prf
   10.27        | _ => prf)
   10.28 -  in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
   10.29 +  in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end;
   10.30  
   10.31  fun pretty_proof ctxt prf =
   10.32    Proof_Context.pretty_term_abbrev
   10.33 @@ -257,6 +257,6 @@
   10.34      (term_of_proof prf);
   10.35  
   10.36  fun pretty_proof_of ctxt full th =
   10.37 -  pretty_proof ctxt (proof_of (Proof_Context.theory_of ctxt) full th);
   10.38 +  pretty_proof ctxt (proof_of ctxt full th);
   10.39  
   10.40  end;
    11.1 --- a/src/Pure/Proof/reconstruct.ML	Sat Apr 09 12:36:25 2016 +0200
    11.2 +++ b/src/Pure/Proof/reconstruct.ML	Sat Apr 09 13:28:32 2016 +0200
    11.3 @@ -6,20 +6,23 @@
    11.4  
    11.5  signature RECONSTRUCT =
    11.6  sig
    11.7 -  val quiet_mode : bool Unsynchronized.ref
    11.8 -  val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
    11.9 +  val quiet_mode : bool Config.T
   11.10 +  val reconstruct_proof : Proof.context -> term -> Proofterm.proof -> Proofterm.proof
   11.11    val prop_of' : term list -> Proofterm.proof -> term
   11.12    val prop_of : Proofterm.proof -> term
   11.13 -  val proof_of : theory -> thm -> Proofterm.proof
   11.14 -  val expand_proof : theory -> (string * term option) list ->
   11.15 +  val proof_of : Proof.context -> thm -> Proofterm.proof
   11.16 +  val expand_proof : Proof.context -> (string * term option) list ->
   11.17      Proofterm.proof -> Proofterm.proof
   11.18  end;
   11.19  
   11.20  structure Reconstruct : RECONSTRUCT =
   11.21  struct
   11.22  
   11.23 -val quiet_mode = Unsynchronized.ref true;
   11.24 -fun message s = if !quiet_mode then () else writeln s;
   11.25 +val quiet_mode =
   11.26 +  Config.bool (Config.declare ("Reconstruct.quiet_mode", @{here}) (K (Config.Bool true)));
   11.27 +
   11.28 +fun message ctxt msg =
   11.29 +  if Config.get ctxt quiet_mode then () else writeln (msg ());
   11.30  
   11.31  fun vars_of t = map Var (rev (Term.add_vars t []));
   11.32  fun frees_of t = map Free (rev (Term.add_frees t []));
   11.33 @@ -43,10 +46,10 @@
   11.34  
   11.35  val mk_abs = fold (fn T => fn u => Abs ("", T, u));
   11.36  
   11.37 -fun unifyT thy env T U =
   11.38 +fun unifyT ctxt env T U =
   11.39    let
   11.40      val Envir.Envir {maxidx, tenv, tyenv} = env;
   11.41 -    val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx);
   11.42 +    val (tyenv', maxidx') = Sign.typ_unify (Proof_Context.theory_of ctxt) (T, U) (tyenv, maxidx);
   11.43    in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end;
   11.44  
   11.45  fun chaseT env (T as TVar v) =
   11.46 @@ -55,9 +58,9 @@
   11.47        | SOME T' => chaseT env T')
   11.48    | chaseT _ T = T;
   11.49  
   11.50 -fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) Ts vTs
   11.51 +fun infer_type ctxt (env as Envir.Envir {maxidx, tenv, tyenv}) Ts vTs
   11.52        (t as Const (s, T)) = if T = dummyT then
   11.53 -        (case Sign.const_type thy s of
   11.54 +        (case Sign.const_type (Proof_Context.theory_of ctxt) s of
   11.55            NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
   11.56          | SOME T =>
   11.57              let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
   11.58 @@ -65,68 +68,69 @@
   11.59                Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv})
   11.60              end)
   11.61        else (t, T, vTs, env)
   11.62 -  | infer_type thy env Ts vTs (t as Free (s, T)) =
   11.63 +  | infer_type ctxt env Ts vTs (t as Free (s, T)) =
   11.64        if T = dummyT then (case Symtab.lookup vTs s of
   11.65            NONE =>
   11.66              let val (T, env') = mk_tvar [] env
   11.67              in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end
   11.68          | SOME T => (Free (s, T), T, vTs, env))
   11.69        else (t, T, vTs, env)
   11.70 -  | infer_type thy env Ts vTs (Var _) = error "reconstruct_proof: internal error"
   11.71 -  | infer_type thy env Ts vTs (Abs (s, T, t)) =
   11.72 +  | infer_type ctxt env Ts vTs (Var _) = error "reconstruct_proof: internal error"
   11.73 +  | infer_type ctxt env Ts vTs (Abs (s, T, t)) =
   11.74        let
   11.75          val (T', env') = if T = dummyT then mk_tvar [] env else (T, env);
   11.76 -        val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t
   11.77 +        val (t', U, vTs', env'') = infer_type ctxt env' (T' :: Ts) vTs t
   11.78        in (Abs (s, T', t'), T' --> U, vTs', env'') end
   11.79 -  | infer_type thy env Ts vTs (t $ u) =
   11.80 +  | infer_type ctxt env Ts vTs (t $ u) =
   11.81        let
   11.82 -        val (t', T, vTs1, env1) = infer_type thy env Ts vTs t;
   11.83 -        val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u;
   11.84 +        val (t', T, vTs1, env1) = infer_type ctxt env Ts vTs t;
   11.85 +        val (u', U, vTs2, env2) = infer_type ctxt env1 Ts vTs1 u;
   11.86        in (case chaseT env2 T of
   11.87 -          Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U')
   11.88 +          Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT ctxt env2 U U')
   11.89          | _ =>
   11.90            let val (V, env3) = mk_tvar [] env2
   11.91 -          in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end)
   11.92 +          in (t' $ u', V, vTs2, unifyT ctxt env3 T (U --> V)) end)
   11.93        end
   11.94 -  | infer_type thy env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env)
   11.95 +  | infer_type ctxt env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env)
   11.96        handle General.Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
   11.97  
   11.98 -fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^
   11.99 -  Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u);
  11.100 +fun cantunify ctxt (t, u) =
  11.101 +  error ("Non-unifiable terms:\n" ^
  11.102 +    Syntax.string_of_term ctxt t ^ "\n\n" ^ Syntax.string_of_term ctxt u);
  11.103  
  11.104 -fun decompose thy Ts (p as (t, u)) env =
  11.105 +fun decompose ctxt Ts (p as (t, u)) env =
  11.106    let
  11.107      fun rigrig (a, T) (b, U) uT ts us =
  11.108 -      if a <> b then cantunify thy p
  11.109 -      else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U))
  11.110 +      if a <> b then cantunify ctxt p
  11.111 +      else apfst flat (fold_map (decompose ctxt Ts) (ts ~~ us) (uT env T U))
  11.112    in
  11.113      case apply2 (strip_comb o Envir.head_norm env) p of
  11.114 -      ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us
  11.115 -    | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us
  11.116 +      ((Const c, ts), (Const d, us)) => rigrig c d (unifyT ctxt) ts us
  11.117 +    | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT ctxt) ts us
  11.118      | ((Bound i, ts), (Bound j, us)) =>
  11.119          rigrig (i, dummyT) (j, dummyT) (K o K) ts us
  11.120      | ((Abs (_, T, t), []), (Abs (_, U, u), [])) =>
  11.121 -        decompose thy (T::Ts) (t, u) (unifyT thy env T U)
  11.122 +        decompose ctxt (T::Ts) (t, u) (unifyT ctxt env T U)
  11.123      | ((Abs (_, T, t), []), _) =>
  11.124 -        decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env
  11.125 +        decompose ctxt (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env
  11.126      | (_, (Abs (_, T, u), [])) =>
  11.127 -        decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env
  11.128 +        decompose ctxt (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env
  11.129      | _ => ([(mk_abs Ts t, mk_abs Ts u)], env)
  11.130    end;
  11.131  
  11.132 -fun make_constraints_cprf thy env cprf =
  11.133 +fun make_constraints_cprf ctxt env cprf =
  11.134    let
  11.135      fun add_cnstrt Ts prop prf cs env vTs (t, u) =
  11.136        let
  11.137          val t' = mk_abs Ts t;
  11.138          val u' = mk_abs Ts u
  11.139        in
  11.140 -        (prop, prf, cs, Pattern.unify (Context.Theory thy) (t', u') env, vTs)
  11.141 +        (prop, prf, cs, Pattern.unify (Context.Proof ctxt) (t', u') env, vTs)
  11.142          handle Pattern.Pattern =>
  11.143 -            let val (cs', env') = decompose thy [] (t', u') env
  11.144 +            let val (cs', env') = decompose ctxt [] (t', u') env
  11.145              in (prop, prf, cs @ cs', env', vTs) end
  11.146          | Pattern.Unif =>
  11.147 -            cantunify thy (Envir.norm_term env t', Envir.norm_term env u')
  11.148 +            cantunify ctxt (Envir.norm_term env t', Envir.norm_term env u')
  11.149        end;
  11.150  
  11.151      fun mk_cnstrts_atom env vTs prop opTs prf =
  11.152 @@ -155,12 +159,13 @@
  11.153                | SOME T => (T, env));
  11.154              val (t, prf, cnstrts, env'', vTs') =
  11.155                mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf;
  11.156 -          in (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf),
  11.157 -            cnstrts, env'', vTs')
  11.158 +          in
  11.159 +            (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf),
  11.160 +              cnstrts, env'', vTs')
  11.161            end
  11.162        | mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) =
  11.163            let
  11.164 -            val (t', _, vTs', env') = infer_type thy env Ts vTs t;
  11.165 +            val (t', _, vTs', env') = infer_type ctxt env Ts vTs t;
  11.166              val (u, prf, cnstrts, env'', vTs'') = mk_cnstrts env' Ts (t'::Hs) vTs' cprf;
  11.167            in (Logic.mk_implies (t', u), AbsP (s, SOME t', prf), cnstrts, env'', vTs'')
  11.168            end
  11.169 @@ -183,11 +188,11 @@
  11.170                  end)
  11.171            end
  11.172        | mk_cnstrts env Ts Hs vTs (cprf % SOME t) =
  11.173 -          let val (t', U, vTs1, env1) = infer_type thy env Ts vTs t
  11.174 +          let val (t', U, vTs1, env1) = infer_type ctxt env Ts vTs t
  11.175            in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of
  11.176               (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
  11.177                   prf, cnstrts, env2, vTs2) =>
  11.178 -               let val env3 = unifyT thy env2 T U
  11.179 +               let val env3 = unifyT ctxt env2 T U
  11.180                 in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2)
  11.181                 end
  11.182             | (u, prf, cnstrts, env2, vTs2) =>
  11.183 @@ -250,12 +255,11 @@
  11.184  (**** solution of constraints ****)
  11.185  
  11.186  fun solve _ [] bigenv = bigenv
  11.187 -  | solve thy cs bigenv =
  11.188 +  | solve ctxt cs bigenv =
  11.189        let
  11.190          fun search env [] = error ("Unsolvable constraints:\n" ^
  11.191                Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
  11.192 -                Thm.pretty_flexpair (Syntax.init_pretty_global thy)
  11.193 -                  (apply2 (Envir.norm_term bigenv) p)) cs)))
  11.194 +                Thm.pretty_flexpair ctxt (apply2 (Envir.norm_term bigenv) p)) cs)))
  11.195            | search env ((u, p as (t1, t2), vs)::ps) =
  11.196                if u then
  11.197                  let
  11.198 @@ -263,10 +267,10 @@
  11.199                    val tn2 = Envir.norm_term bigenv t2
  11.200                  in
  11.201                    if Pattern.pattern tn1 andalso Pattern.pattern tn2 then
  11.202 -                    (Pattern.unify (Context.Theory thy) (tn1, tn2) env, ps) handle Pattern.Unif =>
  11.203 -                       cantunify thy (tn1, tn2)
  11.204 +                    (Pattern.unify (Context.Proof ctxt) (tn1, tn2) env, ps) handle Pattern.Unif =>
  11.205 +                       cantunify ctxt (tn1, tn2)
  11.206                    else
  11.207 -                    let val (cs', env') = decompose thy [] (tn1, tn2) env
  11.208 +                    let val (cs', env') = decompose ctxt [] (tn1, tn2) env
  11.209                      in if cs' = [(tn1, tn2)] then
  11.210                           apsnd (cons (false, (tn1, tn2), vs)) (search env ps)
  11.211                         else search env' (map (fn q => (true, q, vs)) cs' @ ps)
  11.212 @@ -276,23 +280,25 @@
  11.213          val Envir.Envir {maxidx, ...} = bigenv;
  11.214          val (env, cs') = search (Envir.empty maxidx) cs;
  11.215        in
  11.216 -        solve thy (upd_constrs env cs') (Envir.merge (bigenv, env))
  11.217 +        solve ctxt (upd_constrs env cs') (Envir.merge (bigenv, env))
  11.218        end;
  11.219  
  11.220  
  11.221  (**** reconstruction of proofs ****)
  11.222  
  11.223 -fun reconstruct_proof thy prop cprf =
  11.224 +fun reconstruct_proof ctxt prop cprf =
  11.225    let
  11.226      val (cprf' % SOME prop', thawf) = Proofterm.freeze_thaw_prf (cprf % SOME prop);
  11.227 -    val _ = message "Collecting constraints...";
  11.228 -    val (t, prf, cs, env, _) = make_constraints_cprf thy
  11.229 +    val _ = message ctxt (fn _ => "Collecting constraints ...");
  11.230 +    val (t, prf, cs, env, _) = make_constraints_cprf ctxt
  11.231        (Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf';
  11.232      val cs' =
  11.233        map (apply2 (Envir.norm_term env)) ((t, prop') :: cs)
  11.234        |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) [])));
  11.235 -    val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
  11.236 -    val env' = solve thy cs' env
  11.237 +    val _ =
  11.238 +      message ctxt
  11.239 +        (fn () => "Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
  11.240 +    val env' = solve ctxt cs' env
  11.241    in
  11.242      thawf (Proofterm.norm_proof env' prf)
  11.243    end;
  11.244 @@ -324,15 +330,15 @@
  11.245  val prop_of' = Envir.beta_eta_contract oo prop_of0;
  11.246  val prop_of = prop_of' [];
  11.247  
  11.248 -fun proof_of thy raw_thm =
  11.249 -  let val thm = Thm.transfer thy raw_thm
  11.250 -  in reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm) end;
  11.251 +fun proof_of ctxt raw_thm =
  11.252 +  let val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm
  11.253 +  in reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
  11.254  
  11.255  
  11.256  
  11.257  (**** expand and reconstruct subproofs ****)
  11.258  
  11.259 -fun expand_proof thy thms prf =
  11.260 +fun expand_proof ctxt thms prf =
  11.261    let
  11.262      fun expand maxidx prfs (AbsP (s, t, prf)) =
  11.263            let val (maxidx', prfs', prf') = expand maxidx prfs prf
  11.264 @@ -359,10 +365,10 @@
  11.265                  NONE =>
  11.266                    let
  11.267                      val _ =
  11.268 -                      message ("Reconstructing proof of " ^ a ^ "\n" ^
  11.269 -                        Syntax.string_of_term_global thy prop);
  11.270 +                      message ctxt (fn () =>
  11.271 +                        "Reconstructing proof of " ^ a ^ "\n" ^ Syntax.string_of_term ctxt prop);
  11.272                      val prf' = forall_intr_vfs_prf prop
  11.273 -                      (reconstruct_proof thy prop (Proofterm.join_proof body));
  11.274 +                      (reconstruct_proof ctxt prop (Proofterm.join_proof body));
  11.275                      val (maxidx', prfs', prf) = expand
  11.276                        (Proofterm.maxidx_proof prf' ~1) prfs prf'
  11.277                    in (maxidx' + maxidx + 1, Proofterm.incr_indexes (maxidx + 1) prf,