added deriv.ML: Abstract derivations based on raw proof terms.
authorwenzelm
Thu Sep 18 14:06:56 2008 +0200 (2008-09-18)
changeset 2828809c812966e7f
parent 28287 c86fa4e0aedb
child 28289 efd53393412b
added deriv.ML: Abstract derivations based on raw proof terms.
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/deriv.ML
src/Pure/display.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/IsaMakefile	Thu Sep 18 12:13:50 2008 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Thu Sep 18 14:06:56 2008 +0200
     1.3 @@ -76,13 +76,14 @@
     1.4    Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML Tools/quickcheck.ML	\
     1.5    Tools/value.ML Tools/isabelle_process.ML Tools/named_thms.ML		\
     1.6    Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
     1.7 -  conjunction.ML consts.ML context.ML conv.ML defs.ML display.ML	\
     1.8 -  drule.ML envir.ML facts.ML goal.ML interpretation.ML library.ML	\
     1.9 -  logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML	\
    1.10 -  old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML	\
    1.11 -  pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML	\
    1.12 -  tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML	\
    1.13 -  type_infer.ML unify.ML variable.ML
    1.14 +  conjunction.ML consts.ML context.ML conv.ML defs.ML deriv.ML		\
    1.15 +  display.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML	\
    1.16 +  library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML	\
    1.17 +  name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML		\
    1.18 +  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML		\
    1.19 +  simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML	\
    1.20 +  term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML		\
    1.21 +  variable.ML
    1.22  	@./mk
    1.23  
    1.24  
     2.1 --- a/src/Pure/ROOT.ML	Thu Sep 18 12:13:50 2008 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Thu Sep 18 14:06:56 2008 +0200
     2.3 @@ -61,6 +61,7 @@
     2.4  use "theory.ML";
     2.5  use "interpretation.ML";
     2.6  use "proofterm.ML";
     2.7 +use "deriv.ML";
     2.8  use "thm.ML";
     2.9  use "more_thm.ML";
    2.10  use "facts.ML";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/deriv.ML	Thu Sep 18 14:06:56 2008 +0200
     3.3 @@ -0,0 +1,36 @@
     3.4 +(*  Title:      Pure/deriv.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Makarius
     3.7 +
     3.8 +Abstract derivations based on raw proof terms.
     3.9 +*)
    3.10 +
    3.11 +signature DERIV =
    3.12 +sig
    3.13 +  type T
    3.14 +  val oracle_of: T -> bool
    3.15 +  val proof_of: T -> Proofterm.proof
    3.16 +  val uncond_rule: (Proofterm.proof -> Proofterm.proof) -> T -> T
    3.17 +  val rule0: Proofterm.proof -> T
    3.18 +  val rule1: (Proofterm.proof -> Proofterm.proof) -> T -> T
    3.19 +  val rule2: (Proofterm.proof -> Proofterm.proof -> Proofterm.proof) -> T -> T -> T
    3.20 +  val oracle: string -> term -> T
    3.21 +end;
    3.22 +
    3.23 +structure Deriv: DERIV =
    3.24 +struct
    3.25 +
    3.26 +datatype T = Der of bool * Proofterm.proof;
    3.27 +
    3.28 +fun oracle_of (Der (ora, _)) = ora;
    3.29 +fun proof_of (Der (_, proof)) = proof;
    3.30 +
    3.31 +fun uncond_rule f (Der (ora, prf)) = Der (ora, f prf);
    3.32 +
    3.33 +fun rule0 prf = Der (Proofterm.infer_derivs' I (false, prf));
    3.34 +fun rule1 f (Der der) = Der (Proofterm.infer_derivs' f der);
    3.35 +fun rule2 f (Der der1) (Der der2) = Der (Proofterm.infer_derivs f der1 der2);
    3.36 +
    3.37 +fun oracle name prop = Der (true, Proofterm.oracle_proof name prop);
    3.38 +
    3.39 +end;
     4.1 --- a/src/Pure/display.ML	Thu Sep 18 12:13:50 2008 +0200
     4.2 +++ b/src/Pure/display.ML	Thu Sep 18 14:06:56 2008 +0200
     4.3 @@ -61,7 +61,7 @@
     4.4  fun pretty_thm_aux pp quote show_hyps' asms raw_th =
     4.5    let
     4.6      val th = Thm.strip_shyps raw_th;
     4.7 -    val {hyps, tpairs, prop, der = (ora, _), ...} = Thm.rep_thm th;
     4.8 +    val {hyps, tpairs, prop, der, ...} = Thm.rep_thm th;
     4.9      val xshyps = Thm.extra_shyps th;
    4.10      val tags = Thm.get_tags th;
    4.11  
    4.12 @@ -69,7 +69,7 @@
    4.13      val prt_term = q o Pretty.term pp;
    4.14  
    4.15      val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    4.16 -    val ora' = ora andalso (! show_hyps orelse not (! quick_and_dirty));
    4.17 +    val ora' = Deriv.oracle_of der andalso (! show_hyps orelse not (! quick_and_dirty));
    4.18      val hlen = length xshyps + length hyps' + length tpairs;
    4.19      val hsymbs =
    4.20        if hlen = 0 andalso not ora' then []
     5.1 --- a/src/Pure/thm.ML	Thu Sep 18 12:13:50 2008 +0200
     5.2 +++ b/src/Pure/thm.ML	Thu Sep 18 14:06:56 2008 +0200
     5.3 @@ -41,7 +41,7 @@
     5.4    type attribute = Context.generic * thm -> Context.generic * thm
     5.5    val rep_thm: thm ->
     5.6     {thy_ref: theory_ref,
     5.7 -    der: bool * Proofterm.proof,
     5.8 +    der: Deriv.T,
     5.9      tags: Properties.T,
    5.10      maxidx: int,
    5.11      shyps: sort list,
    5.12 @@ -50,7 +50,7 @@
    5.13      prop: term}
    5.14    val crep_thm: thm ->
    5.15     {thy_ref: theory_ref,
    5.16 -    der: bool * Proofterm.proof,
    5.17 +    der: Deriv.T,
    5.18      tags: Properties.T,
    5.19      maxidx: int,
    5.20      shyps: sort list,
    5.21 @@ -337,7 +337,7 @@
    5.22  
    5.23  abstype thm = Thm of
    5.24   {thy_ref: theory_ref,         (*dynamic reference to theory*)
    5.25 -  der: bool * Pt.proof,        (*derivation*)
    5.26 +  der: Deriv.T,                (*derivation*)
    5.27    tags: Properties.T,          (*additional annotations/comments*)
    5.28    maxidx: int,                 (*maximum index of any Var or TVar*)
    5.29    shyps: sort list,            (*sort hypotheses as ordered list*)
    5.30 @@ -394,7 +394,7 @@
    5.31  fun maxidx_thm th i = Int.max (maxidx_of th, i);
    5.32  fun hyps_of (Thm {hyps, ...}) = hyps;
    5.33  fun prop_of (Thm {prop, ...}) = prop;
    5.34 -fun proof_of (Thm {der = (_, proof), ...}) = proof;
    5.35 +fun proof_of (Thm {der, ...}) = Deriv.proof_of der;
    5.36  fun tpairs_of (Thm {tpairs, ...}) = tpairs;
    5.37  
    5.38  val concl_of = Logic.strip_imp_concl o prop_of;
    5.39 @@ -492,7 +492,7 @@
    5.40        Symtab.lookup (Theory.axiom_table thy) name
    5.41        |> Option.map (fn prop =>
    5.42             let
    5.43 -             val der = Pt.infer_derivs' I (false, Pt.axm_proof name prop);
    5.44 +             val der = Deriv.rule0 (Pt.axm_proof name prop);
    5.45               val maxidx = maxidx_of_term prop;
    5.46               val shyps = Sorts.insert_term prop [];
    5.47             in
    5.48 @@ -523,15 +523,15 @@
    5.49  
    5.50  (* official name and additional tags *)
    5.51  
    5.52 -fun get_name (Thm {hyps, prop, der = (_, prf), ...}) =
    5.53 -  Pt.get_name hyps prop prf;
    5.54 +fun get_name (Thm {hyps, prop, der, ...}) =
    5.55 +  Pt.get_name hyps prop (Deriv.proof_of der);
    5.56  
    5.57 -fun put_name name (Thm {thy_ref, der = (ora, prf), tags, maxidx, shyps, hyps, tpairs = [], prop}) =
    5.58 +fun put_name name (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs = [], prop}) =
    5.59        let
    5.60          val thy = Theory.deref thy_ref;
    5.61 -        val der = (ora, Pt.thm_proof thy name hyps prop prf);
    5.62 +        val der' = Deriv.uncond_rule (Pt.thm_proof thy name hyps prop) der;
    5.63        in
    5.64 -        Thm {thy_ref = Theory.check_thy thy, der = der, tags = tags, maxidx = maxidx,
    5.65 +        Thm {thy_ref = Theory.check_thy thy, der = der', tags = tags, maxidx = maxidx,
    5.66            shyps = shyps, hyps = hyps, tpairs = [], prop = prop}
    5.67        end
    5.68    | put_name _ thm = raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
    5.69 @@ -546,9 +546,9 @@
    5.70  fun norm_proof (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
    5.71    let
    5.72      val thy = Theory.deref thy_ref;
    5.73 -    val der = Pt.infer_derivs' (Pt.rew_proof thy) der;
    5.74 +    val der' = Deriv.rule1 (Pt.rew_proof thy) der;
    5.75    in
    5.76 -    Thm {thy_ref = Theory.check_thy thy, der = der, tags = tags, maxidx = maxidx,
    5.77 +    Thm {thy_ref = Theory.check_thy thy, der = der', tags = tags, maxidx = maxidx,
    5.78        shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
    5.79    end;
    5.80  
    5.81 @@ -575,7 +575,7 @@
    5.82      else if maxidx <> ~1 then
    5.83        raise THM ("assume: variables", maxidx, [])
    5.84      else Thm {thy_ref = thy_ref,
    5.85 -      der = Pt.infer_derivs' I (false, Pt.Hyp prop),
    5.86 +      der = Deriv.rule0 (Pt.Hyp prop),
    5.87        tags = [],
    5.88        maxidx = ~1,
    5.89        shyps = sorts,
    5.90 @@ -598,7 +598,7 @@
    5.91      raise THM ("implies_intr: assumptions must have type prop", 0, [th])
    5.92    else
    5.93      Thm {thy_ref = merge_thys1 ct th,
    5.94 -      der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
    5.95 +      der = Deriv.rule1 (Pt.implies_intr_proof A) der,
    5.96        tags = [],
    5.97        maxidx = Int.max (maxidxA, maxidx),
    5.98        shyps = Sorts.union sorts shyps,
    5.99 @@ -623,7 +623,7 @@
   5.100        Const ("==>", _) $ A $ B =>
   5.101          if A aconv propA then
   5.102            Thm {thy_ref = merge_thys2 thAB thA,
   5.103 -            der = Pt.infer_derivs (curry Pt.%%) der derA,
   5.104 +            der = Deriv.rule2 (curry Pt.%%) der derA,
   5.105              tags = [],
   5.106              maxidx = Int.max (maxA, maxidx),
   5.107              shyps = Sorts.union shypsA shyps,
   5.108 @@ -647,7 +647,7 @@
   5.109    let
   5.110      fun result a =
   5.111        Thm {thy_ref = merge_thys1 ct th,
   5.112 -        der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der,
   5.113 +        der = Deriv.rule1 (Pt.forall_intr_proof x a) der,
   5.114          tags = [],
   5.115          maxidx = maxidx,
   5.116          shyps = Sorts.union sorts shyps,
   5.117 @@ -679,7 +679,7 @@
   5.118          raise THM ("forall_elim: type mismatch", 0, [th])
   5.119        else
   5.120          Thm {thy_ref = merge_thys1 ct th,
   5.121 -          der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der,
   5.122 +          der = Deriv.rule1 (Pt.% o rpair (SOME t)) der,
   5.123            tags = [],
   5.124            maxidx = Int.max (maxidx, maxt),
   5.125            shyps = Sorts.union sorts shyps,
   5.126 @@ -696,7 +696,7 @@
   5.127  *)
   5.128  fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
   5.129    Thm {thy_ref = thy_ref,
   5.130 -    der = Pt.infer_derivs' I (false, Pt.reflexive),
   5.131 +    der = Deriv.rule0 Pt.reflexive,
   5.132      tags = [],
   5.133      maxidx = maxidx,
   5.134      shyps = sorts,
   5.135 @@ -713,7 +713,7 @@
   5.136    (case prop of
   5.137      (eq as Const ("==", Type (_, [T, _]))) $ t $ u =>
   5.138        Thm {thy_ref = thy_ref,
   5.139 -        der = Pt.infer_derivs' Pt.symmetric der,
   5.140 +        der = Deriv.rule1 Pt.symmetric der,
   5.141          tags = [],
   5.142          maxidx = maxidx,
   5.143          shyps = shyps,
   5.144 @@ -740,7 +740,7 @@
   5.145          if not (u aconv u') then err "middle term"
   5.146          else
   5.147            Thm {thy_ref = merge_thys2 th1 th2,
   5.148 -            der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
   5.149 +            der = Deriv.rule2 (Pt.transitive u T) der1 der2,
   5.150              tags = [],
   5.151              maxidx = Int.max (max1, max2),
   5.152              shyps = Sorts.union shyps1 shyps2,
   5.153 @@ -762,7 +762,7 @@
   5.154        | _ => raise THM ("beta_conversion: not a redex", 0, []));
   5.155    in
   5.156      Thm {thy_ref = thy_ref,
   5.157 -      der = Pt.infer_derivs' I (false, Pt.reflexive),
   5.158 +      der = Deriv.rule0 Pt.reflexive,
   5.159        tags = [],
   5.160        maxidx = maxidx,
   5.161        shyps = sorts,
   5.162 @@ -773,7 +773,7 @@
   5.163  
   5.164  fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
   5.165    Thm {thy_ref = thy_ref,
   5.166 -    der = Pt.infer_derivs' I (false, Pt.reflexive),
   5.167 +    der = Deriv.rule0 Pt.reflexive,
   5.168      tags = [],
   5.169      maxidx = maxidx,
   5.170      shyps = sorts,
   5.171 @@ -783,7 +783,7 @@
   5.172  
   5.173  fun eta_long_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
   5.174    Thm {thy_ref = thy_ref,
   5.175 -    der = Pt.infer_derivs' I (false, Pt.reflexive),
   5.176 +    der = Deriv.rule0 Pt.reflexive,
   5.177      tags = [],
   5.178      maxidx = maxidx,
   5.179      shyps = sorts,
   5.180 @@ -805,7 +805,7 @@
   5.181        handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
   5.182      val result =
   5.183        Thm {thy_ref = thy_ref,
   5.184 -        der = Pt.infer_derivs' (Pt.abstract_rule x a) der,
   5.185 +        der = Deriv.rule1 (Pt.abstract_rule x a) der,
   5.186          tags = [],
   5.187          maxidx = maxidx,
   5.188          shyps = Sorts.union sorts shyps,
   5.189 @@ -848,7 +848,7 @@
   5.190         Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
   5.191          (chktypes fT tT;
   5.192            Thm {thy_ref = merge_thys2 th1 th2,
   5.193 -            der = Pt.infer_derivs (Pt.combination f g t u fT) der1 der2,
   5.194 +            der = Deriv.rule2 (Pt.combination f g t u fT) der1 der2,
   5.195              tags = [],
   5.196              maxidx = Int.max (max1, max2),
   5.197              shyps = Sorts.union shyps1 shyps2,
   5.198 @@ -875,7 +875,7 @@
   5.199        (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') =>
   5.200          if A aconv A' andalso B aconv B' then
   5.201            Thm {thy_ref = merge_thys2 th1 th2,
   5.202 -            der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2,
   5.203 +            der = Deriv.rule2 (Pt.equal_intr A B) der1 der2,
   5.204              tags = [],
   5.205              maxidx = Int.max (max1, max2),
   5.206              shyps = Sorts.union shyps1 shyps2,
   5.207 @@ -903,7 +903,7 @@
   5.208        Const ("==", _) $ A $ B =>
   5.209          if prop2 aconv A then
   5.210            Thm {thy_ref = merge_thys2 th1 th2,
   5.211 -            der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2,
   5.212 +            der = Deriv.rule2 (Pt.equal_elim A B) der1 der2,
   5.213              tags = [],
   5.214              maxidx = Int.max (max1, max2),
   5.215              shyps = Sorts.union shyps1 shyps2,
   5.216 @@ -932,7 +932,7 @@
   5.217              val tpairs' = tpairs |> map (pairself (Envir.norm_term env))
   5.218                (*remove trivial tpairs, of the form t==t*)
   5.219                |> filter_out (op aconv);
   5.220 -            val der = Pt.infer_derivs' (Pt.norm_proof' env) der;
   5.221 +            val der = Deriv.rule1 (Pt.norm_proof' env) der;
   5.222              val prop' = Envir.norm_term env prop;
   5.223              val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');
   5.224              val shyps = Envir.insert_sorts env shyps;
   5.225 @@ -973,7 +973,7 @@
   5.226        in
   5.227          Thm {
   5.228            thy_ref = thy_ref,
   5.229 -          der = Pt.infer_derivs' (Pt.generalize (tfrees, frees) idx) der,
   5.230 +          der = Deriv.rule1 (Pt.generalize (tfrees, frees) idx) der,
   5.231            tags = [],
   5.232            maxidx = maxidx',
   5.233            shyps = shyps,
   5.234 @@ -1044,7 +1044,7 @@
   5.235            fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
   5.236        in
   5.237          Thm {thy_ref = thy_ref',
   5.238 -          der = Pt.infer_derivs' (fn d =>
   5.239 +          der = Deriv.rule1 (fn d =>
   5.240              Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
   5.241            tags = [],
   5.242            maxidx = maxidx',
   5.243 @@ -1078,7 +1078,7 @@
   5.244      raise THM ("trivial: the term must have type prop", 0, [])
   5.245    else
   5.246      Thm {thy_ref = thy_ref,
   5.247 -      der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)),
   5.248 +      der = Deriv.rule0 (Pt.AbsP ("H", NONE, Pt.PBound 0)),
   5.249        tags = [],
   5.250        maxidx = maxidx,
   5.251        shyps = sorts,
   5.252 @@ -1092,7 +1092,7 @@
   5.253      val Cterm {t, maxidx, sorts, ...} =
   5.254        cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
   5.255          handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   5.256 -    val der = Pt.infer_derivs' I (false, Pt.PAxm ("Pure.class_triv:" ^ c, t, SOME []));
   5.257 +    val der = Deriv.rule0 (Pt.PAxm ("Pure.class_triv:" ^ c, t, SOME []));
   5.258    in
   5.259      Thm {thy_ref = Theory.check_thy thy, der = der, tags = [], maxidx = maxidx,
   5.260        shyps = sorts, hyps = [], tpairs = [], prop = t}
   5.261 @@ -1110,7 +1110,7 @@
   5.262      val constraints = map (curry Logic.mk_inclass T') S;
   5.263    in
   5.264      Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
   5.265 -      der = Pt.infer_derivs' I (false, Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
   5.266 +      der = Deriv.rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
   5.267        tags = [],
   5.268        maxidx = Int.max (maxidx, i),
   5.269        shyps = Sorts.remove_sort S shyps,
   5.270 @@ -1128,7 +1128,7 @@
   5.271      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   5.272    in
   5.273      (al, Thm {thy_ref = thy_ref,
   5.274 -      der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
   5.275 +      der = Deriv.rule1 (Pt.varify_proof prop tfrees) der,
   5.276        tags = [],
   5.277        maxidx = Int.max (0, maxidx),
   5.278        shyps = shyps,
   5.279 @@ -1147,7 +1147,7 @@
   5.280      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   5.281    in
   5.282      Thm {thy_ref = thy_ref,
   5.283 -      der = Pt.infer_derivs' (Pt.freezeT prop1) der,
   5.284 +      der = Deriv.rule1 (Pt.freezeT prop1) der,
   5.285        tags = [],
   5.286        maxidx = maxidx_of_term prop2,
   5.287        shyps = shyps,
   5.288 @@ -1180,7 +1180,7 @@
   5.289      if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, [])
   5.290      else
   5.291        Thm {thy_ref = merge_thys1 goal orule,
   5.292 -        der = Pt.infer_derivs' (Pt.lift_proof gprop inc prop) der,
   5.293 +        der = Deriv.rule1 (Pt.lift_proof gprop inc prop) der,
   5.294          tags = [],
   5.295          maxidx = maxidx + inc,
   5.296          shyps = Sorts.union shyps sorts,  (*sic!*)
   5.297 @@ -1194,8 +1194,7 @@
   5.298    else if i = 0 then thm
   5.299    else
   5.300      Thm {thy_ref = thy_ref,
   5.301 -      der = Pt.infer_derivs'
   5.302 -        (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der,
   5.303 +      der = Deriv.rule1 (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der,
   5.304        tags = [],
   5.305        maxidx = maxidx + i,
   5.306        shyps = shyps,
   5.307 @@ -1211,7 +1210,7 @@
   5.308      val (tpairs, Bs, Bi, C) = dest_state (state, i);
   5.309      fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) =
   5.310        Thm {
   5.311 -        der = Pt.infer_derivs'
   5.312 +        der = Deriv.rule1
   5.313            ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
   5.314              Pt.assumption_proof Bs Bi n) der,
   5.315          tags = [],
   5.316 @@ -1245,7 +1244,7 @@
   5.317        ~1 => raise THM ("eq_assumption", 0, [state])
   5.318      | n =>
   5.319          Thm {thy_ref = thy_ref,
   5.320 -          der = Pt.infer_derivs' (Pt.assumption_proof Bs Bi (n + 1)) der,
   5.321 +          der = Deriv.rule1 (Pt.assumption_proof Bs Bi (n + 1)) der,
   5.322            tags = [],
   5.323            maxidx = maxidx,
   5.324            shyps = shyps,
   5.325 @@ -1274,7 +1273,7 @@
   5.326        else raise THM ("rotate_rule", k, [state]);
   5.327    in
   5.328      Thm {thy_ref = thy_ref,
   5.329 -      der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
   5.330 +      der = Deriv.rule1 (Pt.rotate_proof Bs Bi m) der,
   5.331        tags = [],
   5.332        maxidx = maxidx,
   5.333        shyps = shyps,
   5.334 @@ -1305,7 +1304,7 @@
   5.335        else raise THM ("permute_prems: k", k, [rl]);
   5.336    in
   5.337      Thm {thy_ref = thy_ref,
   5.338 -      der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der,
   5.339 +      der = Deriv.rule1 (Pt.permute_prems_prf prems j m) der,
   5.340        tags = [],
   5.341        maxidx = maxidx,
   5.342        shyps = shyps,
   5.343 @@ -1470,7 +1469,7 @@
   5.344                    (ntps, (map normt (Bs @ As), normt C))
   5.345               end
   5.346             val th =
   5.347 -             Thm{der = Pt.infer_derivs
   5.348 +             Thm{der = Deriv.rule2
   5.349                     ((if Envir.is_empty env then I
   5.350                       else if Envir.above env smax then
   5.351                         (fn f => fn der => f (Pt.norm_proof' env der))
   5.352 @@ -1492,7 +1491,7 @@
   5.353         let val (As1, rder') =
   5.354           if not lifted then (As0, rder)
   5.355           else (map (rename_bvars(dpairs,tpairs,B)) As0,
   5.356 -           Pt.infer_derivs' (Pt.map_proof_terms
   5.357 +           Deriv.rule1 (Pt.map_proof_terms
   5.358               (rename_bvars (dpairs, tpairs, Bound 0)) I) rder);
   5.359         in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
   5.360            handle TERM _ =>
   5.361 @@ -1571,7 +1570,7 @@
   5.362          val thy' = Theory.merge (Theory.deref thy_ref1, thy2);
   5.363          val (prop, T, maxidx) = Sign.certify_term thy' (oracle (thy', data));
   5.364          val shyps' = Sorts.insert_term prop [];
   5.365 -        val der = (true, Pt.oracle_proof name prop);
   5.366 +        val der = Deriv.oracle name prop;
   5.367        in
   5.368          if T <> propT then
   5.369            raise THM ("Oracle's result must have type prop: " ^ name, 0, [])