backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
authorwenzelm
Sun Jun 30 11:37:34 2013 +0200 (2013-06-30 ago)
changeset 5248748bc24467008
parent 52486 b1565e37678b
child 52488 cd65ee49a8ba
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
NEWS
src/Doc/IsarImplementation/Logic.thy
src/HOL/TPTP/ATP_Problem_Import.thy
src/HOL/Tools/Datatype/datatype_realizer.ML
src/Pure/Isar/attrib.ML
src/Pure/ROOT.ML
src/Pure/Tools/build.ML
src/Pure/Tools/proof_general_pure.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/NEWS	Sun Jun 30 11:30:16 2013 +0200
     1.2 +++ b/NEWS	Sun Jun 30 11:37:34 2013 +0200
     1.3 @@ -6,12 +6,11 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 -* Uniform management of "quick_and_dirty" and "proofs" as system
     1.8 -options (see also "isabelle options"), configuration option within the
     1.9 -context (see also Config.get in Isabelle/ML), and attribute in
    1.10 -Isabelle/Isar.  Minor INCOMPATIBILITY, need to use more official
    1.11 -Isabelle means these options, instead of poking into mutable
    1.12 -references.
    1.13 +* Uniform management of "quick_and_dirty" as system option (see also
    1.14 +"isabelle options"), configuration option within the context (see also
    1.15 +Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor
    1.16 +INCOMPATIBILITY, need to use more official Isabelle means to access
    1.17 +quick_and_dirty, instead of historical poking into mutable reference.
    1.18  
    1.19  * Renamed command 'print_configs' to 'print_options'.  Minor
    1.20  INCOMPATIBILITY.
     2.1 --- a/src/Doc/IsarImplementation/Logic.thy	Sun Jun 30 11:30:16 2013 +0200
     2.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Sun Jun 30 11:37:34 2013 +0200
     2.3 @@ -1335,6 +1335,7 @@
     2.4    \begin{mldecls}
     2.5    @{index_ML_type proof} \\
     2.6    @{index_ML_type proof_body} \\
     2.7 +  @{index_ML proofs: "int Unsynchronized.ref"} \\
     2.8    @{index_ML Reconstruct.reconstruct_proof:
     2.9    "theory -> term -> proof -> proof"} \\
    2.10    @{index_ML Reconstruct.expand_proof: "theory ->
    2.11 @@ -1344,10 +1345,6 @@
    2.12    @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
    2.13    \end{mldecls}
    2.14  
    2.15 -  \begin{tabular}{rcll}
    2.16 -  @{attribute_def proofs} & : & @{text attribute} & default @{text 1} \\
    2.17 -  \end{tabular}
    2.18 -
    2.19    \begin{description}
    2.20  
    2.21    \item Type @{ML_type proof} represents proof terms; this is a
    2.22 @@ -1373,6 +1370,13 @@
    2.23    Parallel performance may suffer by inspecting proof terms at
    2.24    run-time.
    2.25  
    2.26 +  \item @{ML proofs} specifies the detail of proof recording within
    2.27 +  @{ML_type thm} values produced by the inference kernel: @{ML 0}
    2.28 +  records only the names of oracles, @{ML 1} records oracle names and
    2.29 +  propositions, @{ML 2} additionally records full proof terms.
    2.30 +  Officially named theorems that contribute to a result are recorded
    2.31 +  in any case.
    2.32 +
    2.33    \item @{ML Reconstruct.reconstruct_proof}~@{text "thy prop prf"}
    2.34    turns the implicit proof term @{text "prf"} into a full proof of the
    2.35    given proposition.
    2.36 @@ -1400,13 +1404,6 @@
    2.37    \item @{ML Proof_Syntax.pretty_proof}~@{text "ctxt prf"}
    2.38    pretty-prints the given proof term.
    2.39  
    2.40 -  \item @{attribute proofs} specifies the detail of proof recording within
    2.41 -  @{ML_type thm} values produced by the inference kernel: @{text 0}
    2.42 -  records only the names of oracles, @{text 1} records oracle names and
    2.43 -  propositions, @{text 2} additionally records full proof terms.
    2.44 -  Officially named theorems that contribute to a result are recorded
    2.45 -  in any case.  %FIXME move to IsarRef
    2.46 -
    2.47    \end{description}
    2.48  *}
    2.49  
     3.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Jun 30 11:30:16 2013 +0200
     3.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Jun 30 11:37:34 2013 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4  
     3.5  ML_file "sledgehammer_tactics.ML"
     3.6  
     3.7 -declare [[proofs = 0]]
     3.8 +ML {* Proofterm.proofs := 0 *}
     3.9  
    3.10  declare [[show_consts]] (* for Refute *)
    3.11  declare [[smt_oracle]]
     4.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sun Jun 30 11:30:16 2013 +0200
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sun Jun 30 11:37:34 2013 +0200
     4.3 @@ -225,7 +225,7 @@
     4.4    end;
     4.5  
     4.6  fun add_dt_realizers config names thy =
     4.7 -  if not (Proofterm.proofs_enabled thy) then thy
     4.8 +  if not (Proofterm.proofs_enabled ()) then thy
     4.9    else
    4.10      let
    4.11        val _ = Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
     5.1 --- a/src/Pure/Isar/attrib.ML	Sun Jun 30 11:30:16 2013 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Sun Jun 30 11:37:34 2013 +0200
     5.3 @@ -554,7 +554,6 @@
     5.4  
     5.5  val _ = Context.>> (Context.map_theory
     5.6   (register_config quick_and_dirty_raw #>
     5.7 -  register_config Proofterm.proofs_raw #>
     5.8    register_config Ast.trace_raw #>
     5.9    register_config Ast.stats_raw #>
    5.10    register_config Printer.show_brackets_raw #>
     6.1 --- a/src/Pure/ROOT.ML	Sun Jun 30 11:30:16 2013 +0200
     6.2 +++ b/src/Pure/ROOT.ML	Sun Jun 30 11:37:34 2013 +0200
     6.3 @@ -341,5 +341,6 @@
     6.4  
     6.5  val cd = File.cd o Path.explode;
     6.6  
     6.7 +Proofterm.proofs := 0;
     6.8  Multithreading.max_threads := 0;
     6.9  
     7.1 --- a/src/Pure/Tools/build.ML	Sun Jun 30 11:30:16 2013 +0200
     7.2 +++ b/src/Pure/Tools/build.ML	Sun Jun 30 11:37:34 2013 +0200
     7.3 @@ -102,6 +102,7 @@
     7.4  
     7.5  fun use_theories last_timing options =
     7.6    Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
     7.7 +    |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
     7.8      |> Unsynchronized.setmp print_mode
     7.9          (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    7.10      |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
     8.1 --- a/src/Pure/Tools/proof_general_pure.ML	Sun Jun 30 11:30:16 2013 +0200
     8.2 +++ b/src/Pure/Tools/proof_general_pure.ML	Sun Jun 30 11:37:34 2013 +0200
     8.3 @@ -152,8 +152,8 @@
     8.4  val _ =
     8.5    ProofGeneral.preference ProofGeneral.category_proof
     8.6      NONE
     8.7 -    (fn () => Markup.print_bool (Markup.parse_int (Options.get_default @{option proofs}) >= 2))
     8.8 -    (fn s => Options.put_default @{option proofs} (if Markup.parse_bool s then "2" else "1"))
     8.9 +    (Markup.print_bool o Proofterm.proofs_enabled)
    8.10 +    (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))
    8.11      ProofGeneral.pgipbool
    8.12      "full-proofs"
    8.13      "Record full proof objects internally";
     9.1 --- a/src/Pure/proofterm.ML	Sun Jun 30 11:30:16 2013 +0200
     9.2 +++ b/src/Pure/proofterm.ML	Sun Jun 30 11:37:34 2013 +0200
     9.3 @@ -8,6 +8,8 @@
     9.4  
     9.5  signature BASIC_PROOFTERM =
     9.6  sig
     9.7 +  val proofs: int Unsynchronized.ref
     9.8 +
     9.9    datatype proof =
    9.10       MinProof
    9.11     | PBound of int
    9.12 @@ -33,10 +35,6 @@
    9.13  sig
    9.14    include BASIC_PROOFTERM
    9.15  
    9.16 -  val proofs_raw: Config.raw
    9.17 -  val proofs: int Config.T
    9.18 -  val proofs_enabled: theory -> bool
    9.19 -
    9.20    type oracle = string * term
    9.21    type pthm = serial * (string * term * proof_body future)
    9.22    val proof_of: proof_body -> proof
    9.23 @@ -61,6 +59,7 @@
    9.24    val decode_body: proof_body XML.Decode.T
    9.25  
    9.26    (** primitive operations **)
    9.27 +  val proofs_enabled: unit -> bool
    9.28    val proof_combt: proof * term list -> proof
    9.29    val proof_combt': proof * term option list -> proof
    9.30    val proof_combP: proof * proof list -> proof
    9.31 @@ -130,12 +129,11 @@
    9.32     {classrel_proof: theory -> class * class -> proof,
    9.33      arity_proof: theory -> string * sort list * class -> proof} -> unit
    9.34    val axm_proof: string -> term -> proof
    9.35 -  val oracle_proof: theory -> string -> term -> oracle * proof
    9.36 +  val oracle_proof: string -> term -> oracle * proof
    9.37  
    9.38    (** rewriting on proof terms **)
    9.39    val add_prf_rrule: proof * proof -> theory -> theory
    9.40 -  val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) ->
    9.41 -    theory -> theory
    9.42 +  val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory
    9.43    val no_skel: proof
    9.44    val normal_skel: proof
    9.45    val rewrite_proof: theory -> (proof * proof) list *
    9.46 @@ -157,16 +155,6 @@
    9.47  structure Proofterm : PROOFTERM =
    9.48  struct
    9.49  
    9.50 -(***** options *****)
    9.51 -
    9.52 -val proofs_raw = Config.declare_option_global "proofs";
    9.53 -val proofs = Config.int proofs_raw;
    9.54 -
    9.55 -fun proofs_enabled thy = Config.get_global thy proofs >= 2;
    9.56 -
    9.57 -val _ = Options.put_default "proofs" "2";  (*compile-time value for Pure*)
    9.58 -
    9.59 -
    9.60  (***** datatype proof *****)
    9.61  
    9.62  datatype proof =
    9.63 @@ -1082,6 +1070,9 @@
    9.64  
    9.65  (***** axioms and theorems *****)
    9.66  
    9.67 +val proofs = Unsynchronized.ref 2;
    9.68 +fun proofs_enabled () = ! proofs >= 2;
    9.69 +
    9.70  fun vars_of t = map Var (rev (Term.add_vars t []));
    9.71  fun frees_of t = map Free (rev (Term.add_frees t []));
    9.72  
    9.73 @@ -1148,9 +1139,8 @@
    9.74  
    9.75  val axm_proof = gen_axm_proof PAxm;
    9.76  
    9.77 -fun oracle_proof thy name prop =
    9.78 -  if Config.get_global thy proofs = 0
    9.79 -  then ((name, Term.dummy), Oracle (name, Term.dummy, NONE))
    9.80 +fun oracle_proof name prop =
    9.81 +  if ! proofs = 0 then ((name, Term.dummy), Oracle (name, Term.dummy, NONE))
    9.82    else ((name, prop), gen_axm_proof Oracle name prop);
    9.83  
    9.84  fun shrink_proof thy =
    9.85 @@ -1561,7 +1551,7 @@
    9.86  
    9.87      fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    9.88      val body0 =
    9.89 -      if not (proofs_enabled thy) then Future.value (make_body0 MinProof)
    9.90 +      if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
    9.91        else if Context.is_draft thy then Future.value (make_body0 (full_proof0 ()))
    9.92        else
    9.93          (singleton o Future.cond_forks)
    10.1 --- a/src/Pure/thm.ML	Sun Jun 30 11:30:16 2013 +0200
    10.2 +++ b/src/Pure/thm.ML	Sun Jun 30 11:37:34 2013 +0200
    10.3 @@ -485,7 +485,7 @@
    10.4  
    10.5  fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
    10.6  
    10.7 -fun deriv_rule2 thy f
    10.8 +fun deriv_rule2 f
    10.9      (Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
   10.10      (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
   10.11    let
   10.12 @@ -493,15 +493,15 @@
   10.13      val oras = Proofterm.unions_oracles [oras1, oras2];
   10.14      val thms = Proofterm.unions_thms [thms1, thms2];
   10.15      val prf =
   10.16 -      (case Config.get_global thy Proofterm.proofs of
   10.17 +      (case ! Proofterm.proofs of
   10.18          2 => f prf1 prf2
   10.19        | 1 => MinProof
   10.20        | 0 => MinProof
   10.21        | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
   10.22    in make_deriv ps oras thms prf end;
   10.23  
   10.24 -fun deriv_rule1 thy f = deriv_rule2 thy (K f) empty_deriv;
   10.25 -fun deriv_rule0 thy prf = deriv_rule1 thy I (make_deriv [] [] [] prf);
   10.26 +fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
   10.27 +fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
   10.28  
   10.29  fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
   10.30    make_deriv promises oracles thms (f proof);
   10.31 @@ -615,7 +615,7 @@
   10.32        Symtab.lookup (Theory.axiom_table thy) name
   10.33        |> Option.map (fn prop =>
   10.34             let
   10.35 -             val der = deriv_rule0 theory (Proofterm.axm_proof name prop);
   10.36 +             val der = deriv_rule0 (Proofterm.axm_proof name prop);
   10.37               val maxidx = maxidx_of_term prop;
   10.38               val shyps = Sorts.insert_term prop [];
   10.39             in
   10.40 @@ -647,7 +647,7 @@
   10.41  fun norm_proof (Thm (der, args as {thy_ref, ...})) =
   10.42    let
   10.43      val thy = Theory.deref thy_ref;
   10.44 -    val der' = deriv_rule1 thy (Proofterm.rew_proof thy) der;
   10.45 +    val der' = deriv_rule1 (Proofterm.rew_proof thy) der;
   10.46      val _ = Theory.check_thy thy;
   10.47    in Thm (der', args) end;
   10.48  
   10.49 @@ -673,7 +673,7 @@
   10.50        raise THM ("assume: prop", 0, [])
   10.51      else if maxidx <> ~1 then
   10.52        raise THM ("assume: variables", maxidx, [])
   10.53 -    else Thm (deriv_rule0 (Theory.deref thy_ref) (Proofterm.Hyp prop),
   10.54 +    else Thm (deriv_rule0 (Proofterm.Hyp prop),
   10.55       {thy_ref = thy_ref,
   10.56        tags = [],
   10.57        maxidx = ~1,
   10.58 @@ -696,16 +696,14 @@
   10.59    if T <> propT then
   10.60      raise THM ("implies_intr: assumptions must have type prop", 0, [th])
   10.61    else
   10.62 -    let val thy_ref = merge_thys1 ct th in
   10.63 -      Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.implies_intr_proof A) der,
   10.64 -       {thy_ref = thy_ref,
   10.65 -        tags = [],
   10.66 -        maxidx = Int.max (maxidxA, maxidx),
   10.67 -        shyps = Sorts.union sorts shyps,
   10.68 -        hyps = remove_hyps A hyps,
   10.69 -        tpairs = tpairs,
   10.70 -        prop = Logic.mk_implies (A, prop)})
   10.71 -    end;
   10.72 +    Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der,
   10.73 +     {thy_ref = merge_thys1 ct th,
   10.74 +      tags = [],
   10.75 +      maxidx = Int.max (maxidxA, maxidx),
   10.76 +      shyps = Sorts.union sorts shyps,
   10.77 +      hyps = remove_hyps A hyps,
   10.78 +      tpairs = tpairs,
   10.79 +      prop = Logic.mk_implies (A, prop)});
   10.80  
   10.81  
   10.82  (*Implication elimination
   10.83 @@ -719,13 +717,12 @@
   10.84        prop = propA, ...}) = thA
   10.85      and Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...}) = thAB;
   10.86      fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
   10.87 -    val thy_ref = merge_thys2 thAB thA;
   10.88    in
   10.89      case prop of
   10.90        Const ("==>", _) $ A $ B =>
   10.91          if A aconv propA then
   10.92 -          Thm (deriv_rule2 (Theory.deref thy_ref) (curry Proofterm.%%) der derA,
   10.93 -           {thy_ref = thy_ref,
   10.94 +          Thm (deriv_rule2 (curry Proofterm.%%) der derA,
   10.95 +           {thy_ref = merge_thys2 thAB thA,
   10.96              tags = [],
   10.97              maxidx = Int.max (maxA, maxidx),
   10.98              shyps = Sorts.union shypsA shyps,
   10.99 @@ -747,10 +744,9 @@
  10.100      (ct as Cterm {t = x, T, sorts, ...})
  10.101      (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
  10.102    let
  10.103 -    val thy_ref = merge_thys1 ct th;
  10.104      fun result a =
  10.105 -      Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.forall_intr_proof x a) der,
  10.106 -       {thy_ref = thy_ref,
  10.107 +      Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,
  10.108 +       {thy_ref = merge_thys1 ct th,
  10.109          tags = [],
  10.110          maxidx = maxidx,
  10.111          shyps = Sorts.union sorts shyps,
  10.112 @@ -781,16 +777,14 @@
  10.113        if T <> qary then
  10.114          raise THM ("forall_elim: type mismatch", 0, [th])
  10.115        else
  10.116 -        let val thy_ref = merge_thys1 ct th in
  10.117 -          Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.% o rpair (SOME t)) der,
  10.118 -           {thy_ref = thy_ref,
  10.119 -            tags = [],
  10.120 -            maxidx = Int.max (maxidx, maxt),
  10.121 -            shyps = Sorts.union sorts shyps,
  10.122 -            hyps = hyps,
  10.123 -            tpairs = tpairs,
  10.124 -            prop = Term.betapply (A, t)})
  10.125 -        end
  10.126 +        Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der,
  10.127 +         {thy_ref = merge_thys1 ct th,
  10.128 +          tags = [],
  10.129 +          maxidx = Int.max (maxidx, maxt),
  10.130 +          shyps = Sorts.union sorts shyps,
  10.131 +          hyps = hyps,
  10.132 +          tpairs = tpairs,
  10.133 +          prop = Term.betapply (A, t)})
  10.134    | _ => raise THM ("forall_elim: not quantified", 0, [th]));
  10.135  
  10.136  
  10.137 @@ -800,7 +794,7 @@
  10.138    t == t
  10.139  *)
  10.140  fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
  10.141 -  Thm (deriv_rule0 (Theory.deref thy_ref) Proofterm.reflexive,
  10.142 +  Thm (deriv_rule0 Proofterm.reflexive,
  10.143     {thy_ref = thy_ref,
  10.144      tags = [],
  10.145      maxidx = maxidx,
  10.146 @@ -817,7 +811,7 @@
  10.147  fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
  10.148    (case prop of
  10.149      (eq as Const ("==", _)) $ t $ u =>
  10.150 -      Thm (deriv_rule1 (Theory.deref thy_ref) Proofterm.symmetric der,
  10.151 +      Thm (deriv_rule1 Proofterm.symmetric der,
  10.152         {thy_ref = thy_ref,
  10.153          tags = [],
  10.154          maxidx = maxidx,
  10.155 @@ -839,14 +833,13 @@
  10.156      and Thm (der2, {maxidx = max2, hyps = hyps2, shyps = shyps2, tpairs = tpairs2,
  10.157        prop = prop2, ...}) = th2;
  10.158      fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
  10.159 -    val thy_ref = merge_thys2 th1 th2;
  10.160    in
  10.161      case (prop1, prop2) of
  10.162        ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) =>
  10.163          if not (u aconv u') then err "middle term"
  10.164          else
  10.165 -          Thm (deriv_rule2 (Theory.deref thy_ref) (Proofterm.transitive u T) der1 der2,
  10.166 -           {thy_ref = thy_ref,
  10.167 +          Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
  10.168 +           {thy_ref = merge_thys2 th1 th2,
  10.169              tags = [],
  10.170              maxidx = Int.max (max1, max2),
  10.171              shyps = Sorts.union shyps1 shyps2,
  10.172 @@ -867,7 +860,7 @@
  10.173        (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
  10.174        | _ => raise THM ("beta_conversion: not a redex", 0, []));
  10.175    in
  10.176 -    Thm (deriv_rule0 (Theory.deref thy_ref) Proofterm.reflexive,
  10.177 +    Thm (deriv_rule0 Proofterm.reflexive,
  10.178       {thy_ref = thy_ref,
  10.179        tags = [],
  10.180        maxidx = maxidx,
  10.181 @@ -878,7 +871,7 @@
  10.182    end;
  10.183  
  10.184  fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
  10.185 -  Thm (deriv_rule0 (Theory.deref thy_ref) Proofterm.reflexive,
  10.186 +  Thm (deriv_rule0 Proofterm.reflexive,
  10.187     {thy_ref = thy_ref,
  10.188      tags = [],
  10.189      maxidx = maxidx,
  10.190 @@ -888,7 +881,7 @@
  10.191      prop = Logic.mk_equals (t, Envir.eta_contract t)});
  10.192  
  10.193  fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
  10.194 -  Thm (deriv_rule0 (Theory.deref thy_ref) Proofterm.reflexive,
  10.195 +  Thm (deriv_rule0 Proofterm.reflexive,
  10.196     {thy_ref = thy_ref,
  10.197      tags = [],
  10.198      maxidx = maxidx,
  10.199 @@ -910,7 +903,7 @@
  10.200      val (t, u) = Logic.dest_equals prop
  10.201        handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
  10.202      val result =
  10.203 -      Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.abstract_rule x a) der,
  10.204 +      Thm (deriv_rule1 (Proofterm.abstract_rule x a) der,
  10.205         {thy_ref = thy_ref,
  10.206          tags = [],
  10.207          maxidx = maxidx,
  10.208 @@ -948,14 +941,13 @@
  10.209              raise THM ("combination: types", 0, [th1, th2])
  10.210            else ()
  10.211        | _ => raise THM ("combination: not function type", 0, [th1, th2]));
  10.212 -    val thy_ref = merge_thys2 th1 th2;
  10.213    in
  10.214      case (prop1, prop2) of
  10.215        (Const ("==", Type ("fun", [fT, _])) $ f $ g,
  10.216         Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
  10.217          (chktypes fT tT;
  10.218 -          Thm (deriv_rule2 (Theory.deref thy_ref) (Proofterm.combination f g t u fT) der1 der2,
  10.219 -           {thy_ref = thy_ref,
  10.220 +          Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
  10.221 +           {thy_ref = merge_thys2 th1 th2,
  10.222              tags = [],
  10.223              maxidx = Int.max (max1, max2),
  10.224              shyps = Sorts.union shyps1 shyps2,
  10.225 @@ -977,13 +969,12 @@
  10.226      and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
  10.227        prop = prop2, ...}) = th2;
  10.228      fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]);
  10.229 -    val thy_ref = merge_thys2 th1 th2;
  10.230    in
  10.231      case (prop1, prop2) of
  10.232        (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') =>
  10.233          if A aconv A' andalso B aconv B' then
  10.234 -          Thm (deriv_rule2 (Theory.deref thy_ref) (Proofterm.equal_intr A B) der1 der2,
  10.235 -           {thy_ref = thy_ref,
  10.236 +          Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
  10.237 +           {thy_ref = merge_thys2 th1 th2,
  10.238              tags = [],
  10.239              maxidx = Int.max (max1, max2),
  10.240              shyps = Sorts.union shyps1 shyps2,
  10.241 @@ -1006,13 +997,12 @@
  10.242      and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2,
  10.243        tpairs = tpairs2, prop = prop2, ...}) = th2;
  10.244      fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]);
  10.245 -    val thy_ref = merge_thys2 th1 th2;
  10.246    in
  10.247      case prop1 of
  10.248        Const ("==", _) $ A $ B =>
  10.249          if prop2 aconv A then
  10.250 -          Thm (deriv_rule2 (Theory.deref thy_ref) (Proofterm.equal_elim A B) der1 der2,
  10.251 -           {thy_ref = thy_ref,
  10.252 +          Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
  10.253 +           {thy_ref = merge_thys2 th1 th2,
  10.254              tags = [],
  10.255              maxidx = Int.max (max1, max2),
  10.256              shyps = Sorts.union shyps1 shyps2,
  10.257 @@ -1041,7 +1031,7 @@
  10.258              val tpairs' = tpairs |> map (pairself (Envir.norm_term env))
  10.259                (*remove trivial tpairs, of the form t==t*)
  10.260                |> filter_out (op aconv);
  10.261 -            val der' = deriv_rule1 thy (Proofterm.norm_proof' env) der;
  10.262 +            val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
  10.263              val prop' = Envir.norm_term env prop;
  10.264              val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');
  10.265              val shyps = Envir.insert_sorts env shyps;
  10.266 @@ -1081,7 +1071,7 @@
  10.267          val tpairs' = map (pairself gen) tpairs;
  10.268          val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
  10.269        in
  10.270 -        Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.generalize (tfrees, frees) idx) der,
  10.271 +        Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der,
  10.272           {thy_ref = thy_ref,
  10.273            tags = [],
  10.274            maxidx = maxidx',
  10.275 @@ -1152,7 +1142,7 @@
  10.276          val (tpairs', maxidx') =
  10.277            fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
  10.278        in
  10.279 -        Thm (deriv_rule1 (Theory.deref thy_ref')
  10.280 +        Thm (deriv_rule1
  10.281            (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
  10.282           {thy_ref = thy_ref',
  10.283            tags = [],
  10.284 @@ -1186,7 +1176,7 @@
  10.285    if T <> propT then
  10.286      raise THM ("trivial: the term must have type prop", 0, [])
  10.287    else
  10.288 -    Thm (deriv_rule0 (Theory.deref thy_ref) (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
  10.289 +    Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
  10.290       {thy_ref = thy_ref,
  10.291        tags = [],
  10.292        maxidx = maxidx,
  10.293 @@ -1208,7 +1198,7 @@
  10.294      val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c));
  10.295    in
  10.296      if Sign.of_sort thy (T, [c]) then
  10.297 -      Thm (deriv_rule0 thy (Proofterm.OfClass (T, c)),
  10.298 +      Thm (deriv_rule0 (Proofterm.OfClass (T, c)),
  10.299         {thy_ref = Theory.check_thy thy,
  10.300          tags = [],
  10.301          maxidx = maxidx,
  10.302 @@ -1276,7 +1266,7 @@
  10.303      val (al, prop2) = Type.varify_global tfrees prop1;
  10.304      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
  10.305    in
  10.306 -    (al, Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.varify_proof prop tfrees) der,
  10.307 +    (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der,
  10.308       {thy_ref = thy_ref,
  10.309        tags = [],
  10.310        maxidx = Int.max (0, maxidx),
  10.311 @@ -1295,7 +1285,7 @@
  10.312      val prop2 = Type.legacy_freeze prop1;
  10.313      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
  10.314    in
  10.315 -    Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.legacy_freezeT prop1) der,
  10.316 +    Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der,
  10.317       {thy_ref = thy_ref,
  10.318        tags = [],
  10.319        maxidx = maxidx_of_term prop2,
  10.320 @@ -1316,7 +1306,7 @@
  10.321    handle TERM _ => raise THM("dest_state", i, [state]);
  10.322  
  10.323  (*Prepare orule for resolution by lifting it over the parameters and
  10.324 -  assumptions of goal.*)
  10.325 +assumptions of goal.*)
  10.326  fun lift_rule goal orule =
  10.327    let
  10.328      val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal;
  10.329 @@ -1325,12 +1315,11 @@
  10.330      val lift_all = Logic.lift_all inc gprop;
  10.331      val Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...}) = orule;
  10.332      val (As, B) = Logic.strip_horn prop;
  10.333 -    val thy_ref = merge_thys1 goal orule;
  10.334    in
  10.335      if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, [])
  10.336      else
  10.337 -      Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.lift_proof gprop inc prop) der,
  10.338 -       {thy_ref = thy_ref,
  10.339 +      Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der,
  10.340 +       {thy_ref = merge_thys1 goal orule,
  10.341          tags = [],
  10.342          maxidx = maxidx + inc,
  10.343          shyps = Sorts.union shyps sorts,  (*sic!*)
  10.344 @@ -1343,7 +1332,7 @@
  10.345    if i < 0 then raise THM ("negative increment", 0, [thm])
  10.346    else if i = 0 then thm
  10.347    else
  10.348 -    Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.incr_indexes i) der,
  10.349 +    Thm (deriv_rule1 (Proofterm.incr_indexes i) der,
  10.350       {thy_ref = thy_ref,
  10.351        tags = [],
  10.352        maxidx = maxidx + i,
  10.353 @@ -1359,7 +1348,7 @@
  10.354      val thy = Theory.deref thy_ref;
  10.355      val (tpairs, Bs, Bi, C) = dest_state (state, i);
  10.356      fun newth n (env, tpairs) =
  10.357 -      Thm (deriv_rule1 thy
  10.358 +      Thm (deriv_rule1
  10.359            ((if Envir.is_empty env then I else (Proofterm.norm_proof' env)) o
  10.360              Proofterm.assumption_proof Bs Bi n) der,
  10.361         {tags = [],
  10.362 @@ -1398,7 +1387,7 @@
  10.363      (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of
  10.364        ~1 => raise THM ("eq_assumption", 0, [state])
  10.365      | n =>
  10.366 -        Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.assumption_proof Bs Bi (n + 1)) der,
  10.367 +        Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der,
  10.368           {thy_ref = thy_ref,
  10.369            tags = [],
  10.370            maxidx = maxidx,
  10.371 @@ -1427,7 +1416,7 @@
  10.372          in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
  10.373        else raise THM ("rotate_rule", k, [state]);
  10.374    in
  10.375 -    Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.rotate_proof Bs Bi m) der,
  10.376 +    Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der,
  10.377       {thy_ref = thy_ref,
  10.378        tags = [],
  10.379        maxidx = maxidx,
  10.380 @@ -1458,7 +1447,7 @@
  10.381          in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
  10.382        else raise THM ("permute_prems: k", k, [rl]);
  10.383    in
  10.384 -    Thm (deriv_rule1 (Theory.deref thy_ref) (Proofterm.permute_prems_proof prems j m) der,
  10.385 +    Thm (deriv_rule1 (Proofterm.permute_prems_proof prems j m) der,
  10.386       {thy_ref = thy_ref,
  10.387        tags = [],
  10.388        maxidx = maxidx,
  10.389 @@ -1652,7 +1641,7 @@
  10.390                    (ntps, (map normt (Bs @ As), normt C))
  10.391               end
  10.392             val th =
  10.393 -             Thm (deriv_rule2 thy
  10.394 +             Thm (deriv_rule2
  10.395                     ((if Envir.is_empty env then I
  10.396                       else if Envir.above env smax then
  10.397                         (fn f => fn der => f (Proofterm.norm_proof' env der))
  10.398 @@ -1676,7 +1665,7 @@
  10.399           else
  10.400             let val rename = rename_bvars dpairs tpairs B As0
  10.401             in (map (rename strip_apply) As0,
  10.402 -             deriv_rule1 thy (Proofterm.map_proof_terms (rename K) I) rder)
  10.403 +             deriv_rule1 (Proofterm.map_proof_terms (rename K) I) rder)
  10.404             end;
  10.405         in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
  10.406            handle TERM _ =>
  10.407 @@ -1765,12 +1754,9 @@
  10.408      if T <> propT then
  10.409        raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
  10.410      else
  10.411 -      let
  10.412 -        val thy_ref = Theory.merge_refs (thy_ref1, thy_ref2);
  10.413 -        val (ora, prf) = Proofterm.oracle_proof (Theory.deref thy_ref) name prop;
  10.414 -      in
  10.415 +      let val (ora, prf) = Proofterm.oracle_proof name prop in
  10.416          Thm (make_deriv [] [ora] [] prf,
  10.417 -         {thy_ref = thy_ref,
  10.418 +         {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
  10.419            tags = [],
  10.420            maxidx = maxidx,
  10.421            shyps = sorts,