src/Pure/thm.ML

 end;
 
 structure Thm: THM =
 struct
 
-structure Pt = Proofterm;
-
-
 (*** Certified terms and types ***)
 
 (** certified types **)
 
 abstype ctyp = Ctyp of

   hyps: term OrdList.T,                         (*hypotheses*)
   tpairs: (term * term) list,                   (*flex-flex pairs*)
   prop: term}                                   (*conclusion*)
 and deriv = Deriv of
  {promises: (serial * thm future) OrdList.T,
-  body: Pt.proof_body}
+  body: Proofterm.proof_body}
 with
 
 type conv = cterm -> thm;
 
 (*attributes subsume any kind of rules or context modifiers*)

 (** derivations and promised proofs **)
 
 fun make_deriv promises oracles thms proof =
   Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
 
-val empty_deriv = make_deriv [] [] [] Pt.MinProof;
+val empty_deriv = make_deriv [] [] [] Proofterm.MinProof;
 
 
 (* inference rules *)
 
 fun promise_ord ((i, _), (j, _)) = int_ord (j, i);

 fun deriv_rule2 f
     (Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
     (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
   let
     val ps = OrdList.union promise_ord ps1 ps2;
-    val oras = Pt.merge_oracles oras1 oras2;
-    val thms = Pt.merge_thms thms1 thms2;
+    val oras = Proofterm.merge_oracles oras1 oras2;
+    val thms = Proofterm.merge_thms thms1 thms2;
     val prf =
-      (case ! Pt.proofs of
+      (case ! Proofterm.proofs of
         2 => f prf1 prf2
       | 1 => MinProof
       | 0 => MinProof
       | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
   in make_deriv ps oras thms prf end;

 (* fulfilled proofs *)
 
 fun raw_body (Thm (Deriv {body, ...}, _)) = body;
 
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
-  Pt.fulfill_norm_proof (Theory.deref thy_ref)
+  Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
 and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
 
-val join_proofs = Pt.join_bodies o map fulfill_body;
-
-fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
-val proof_of = Pt.proof_of o proof_body_of;
+val join_proofs = Proofterm.join_bodies o map fulfill_body;
+
+fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);
+val proof_of = Proofterm.proof_of o proof_body_of;
 
 
 (* derivation status *)
 
 fun status_of (Thm (Deriv {promises, body}, _)) =
   let
     val ps = map (Future.peek o snd) promises;
     val bodies = body ::
       map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
-    val {oracle, unfinished, failed} = Pt.status_of bodies;
+    val {oracle, unfinished, failed} = Proofterm.status_of bodies;
   in
    {oracle = oracle,
     unfinished = unfinished orelse exists is_none ps,
     failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
   end;

     val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
 
     val i = serial ();
     val future = future_thm |> Future.map (future_result i thy sorts prop);
   in
-    Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop),
+    Thm (make_deriv [(i, future)] [] [] (Proofterm.promise_proof thy i prop),
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx,
       shyps = sorts,
       hyps = [],

 
 
 (* closed derivations with official name *)
 
 fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
-  Pt.get_name shyps hyps prop (Pt.proof_of body);
+  Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
 
 fun name_derivation name (thm as Thm (der, args)) =
   let
     val Deriv {promises, body} = der;
     val {thy_ref, shyps, hyps, prop, tpairs, ...} = args;
     val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
 
     val ps = map (apsnd (Future.map proof_body_of)) promises;
     val thy = Theory.deref thy_ref;
-    val (pthm, proof) = Pt.thm_proof thy name shyps hyps prop ps body;
+    val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body;
     val der' = make_deriv [] [] [pthm] proof;
     val _ = Theory.check_thy thy;
   in Thm (der', args) end;
 
 

   let
     fun get_ax thy =
       Symtab.lookup (Theory.axiom_table thy) name
       |> Option.map (fn prop =>
            let
-             val der = deriv_rule0 (Pt.axm_proof name prop);
+             val der = deriv_rule0 (Proofterm.axm_proof name prop);
              val maxidx = maxidx_of_term prop;
              val shyps = Sorts.insert_term prop [];
            in
              Thm (der, {thy_ref = Theory.check_thy thy, tags = [],
                maxidx = maxidx, shyps = shyps, hyps = [], tpairs = [], prop = prop})

 
 
 fun norm_proof (Thm (der, args as {thy_ref, ...})) =
   let
     val thy = Theory.deref thy_ref;
-    val der' = deriv_rule1 (Pt.rew_proof thy) der;
+    val der' = deriv_rule1 (Proofterm.rew_proof thy) der;
     val _ = Theory.check_thy thy;
   in Thm (der', args) end;
 
 fun adjust_maxidx_thm i (th as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
   if maxidx = i then th

   let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in
     if T <> propT then
       raise THM ("assume: prop", 0, [])
     else if maxidx <> ~1 then
       raise THM ("assume: variables", maxidx, [])
-    else Thm (deriv_rule0 (Pt.Hyp prop),
+    else Thm (deriv_rule0 (Proofterm.Hyp prop),
      {thy_ref = thy_ref,
       tags = [],
       maxidx = ~1,
       shyps = sorts,
       hyps = [prop],

     (ct as Cterm {t = A, T, maxidx = maxidxA, sorts, ...})
     (th as Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...})) =
   if T <> propT then
     raise THM ("implies_intr: assumptions must have type prop", 0, [th])
   else
-    Thm (deriv_rule1 (Pt.implies_intr_proof A) der,
+    Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der,
      {thy_ref = merge_thys1 ct th,
       tags = [],
       maxidx = Int.max (maxidxA, maxidx),
       shyps = Sorts.union sorts shyps,
       hyps = remove_hyps A hyps,

     fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
   in
     case prop of
       Const ("==>", _) $ A $ B =>
         if A aconv propA then
-          Thm (deriv_rule2 (curry Pt.%%) der derA,
+          Thm (deriv_rule2 (curry Proofterm.%%) der derA,
            {thy_ref = merge_thys2 thAB thA,
             tags = [],
             maxidx = Int.max (maxA, maxidx),
             shyps = Sorts.union shypsA shyps,
             hyps = union_hyps hypsA hyps,

 fun forall_intr
     (ct as Cterm {t = x, T, sorts, ...})
     (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
   let
     fun result a =
-      Thm (deriv_rule1 (Pt.forall_intr_proof x a) der,
+      Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,
        {thy_ref = merge_thys1 ct th,
         tags = [],
         maxidx = maxidx,
         shyps = Sorts.union sorts shyps,
         hyps = hyps,

   (case prop of
     Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
       if T <> qary then
         raise THM ("forall_elim: type mismatch", 0, [th])
       else
-        Thm (deriv_rule1 (Pt.% o rpair (SOME t)) der,
+        Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der,
          {thy_ref = merge_thys1 ct th,
           tags = [],
           maxidx = Int.max (maxidx, maxt),
           shyps = Sorts.union sorts shyps,
           hyps = hyps,

 
 (*Reflexivity
   t == t
 *)
 fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 Pt.reflexive,
+  Thm (deriv_rule0 Proofterm.reflexive,
    {thy_ref = thy_ref,
     tags = [],
     maxidx = maxidx,
     shyps = sorts,
     hyps = [],

   u == t
 *)
 fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
   (case prop of
     (eq as Const ("==", _)) $ t $ u =>
-      Thm (deriv_rule1 Pt.symmetric der,
+      Thm (deriv_rule1 Proofterm.symmetric der,
        {thy_ref = thy_ref,
         tags = [],
         maxidx = maxidx,
         shyps = shyps,
         hyps = hyps,

   in
     case (prop1, prop2) of
       ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) =>
         if not (u aconv u') then err "middle term"
         else
-          Thm (deriv_rule2 (Pt.transitive u T) der1 der2,
+          Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
            {thy_ref = merge_thys2 th1 th2,
             tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,

     if full then Envir.beta_norm t
     else
       (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
       | _ => raise THM ("beta_conversion: not a redex", 0, []));
   in
-    Thm (deriv_rule0 Pt.reflexive,
+    Thm (deriv_rule0 Proofterm.reflexive,
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx,
       shyps = sorts,
       hyps = [],
       tpairs = [],
       prop = Logic.mk_equals (t, t')})
   end;
 
 fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 Pt.reflexive,
+  Thm (deriv_rule0 Proofterm.reflexive,
    {thy_ref = thy_ref,
     tags = [],
     maxidx = maxidx,
     shyps = sorts,
     hyps = [],
     tpairs = [],
     prop = Logic.mk_equals (t, Envir.eta_contract t)});
 
 fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 Pt.reflexive,
+  Thm (deriv_rule0 Proofterm.reflexive,
    {thy_ref = thy_ref,
     tags = [],
     maxidx = maxidx,
     shyps = sorts,
     hyps = [],

     (th as Thm (der, {thy_ref, maxidx, hyps, shyps, tpairs, prop, ...})) =
   let
     val (t, u) = Logic.dest_equals prop
       handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
     val result =
-      Thm (deriv_rule1 (Pt.abstract_rule x a) der,
+      Thm (deriv_rule1 (Proofterm.abstract_rule x a) der,
        {thy_ref = thy_ref,
         tags = [],
         maxidx = maxidx,
         shyps = Sorts.union sorts shyps,
         hyps = hyps,

   in
     case (prop1, prop2) of
       (Const ("==", Type ("fun", [fT, _])) $ f $ g,
        Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
         (chktypes fT tT;
-          Thm (deriv_rule2 (Pt.combination f g t u fT) der1 der2,
+          Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
            {thy_ref = merge_thys2 th1 th2,
             tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,

     fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]);
   in
     case (prop1, prop2) of
       (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') =>
         if A aconv A' andalso B aconv B' then
-          Thm (deriv_rule2 (Pt.equal_intr A B) der1 der2,
+          Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
            {thy_ref = merge_thys2 th1 th2,
             tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,

     fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]);
   in
     case prop1 of
       Const ("==", _) $ A $ B =>
         if prop2 aconv A then
-          Thm (deriv_rule2 (Pt.equal_elim A B) der1 der2,
+          Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
            {thy_ref = merge_thys2 th1 th2,
             tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,

         else
           let
             val tpairs' = tpairs |> map (pairself (Envir.norm_term env))
               (*remove trivial tpairs, of the form t==t*)
               |> filter_out (op aconv);
-            val der' = deriv_rule1 (Pt.norm_proof' env) der;
+            val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
             val prop' = Envir.norm_term env prop;
             val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');
             val shyps = Envir.insert_sorts env shyps;
           in
             Thm (der', {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx,

         val gen = Term_Subst.generalize (tfrees, frees) idx;
         val prop' = gen prop;
         val tpairs' = map (pairself gen) tpairs;
         val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
       in
-        Thm (deriv_rule1 (Pt.generalize (tfrees, frees) idx) der,
+        Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der,
          {thy_ref = thy_ref,
           tags = [],
           maxidx = maxidx',
           shyps = shyps,
           hyps = hyps,

         val subst = Term_Subst.instantiate_maxidx (instT', inst');
         val (prop', maxidx1) = subst prop ~1;
         val (tpairs', maxidx') =
           fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
       in
-        Thm (deriv_rule1 (fn d => Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
+        Thm (deriv_rule1
+          (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
          {thy_ref = thy_ref',
           tags = [],
           maxidx = maxidx',
           shyps = shyps',
           hyps = hyps,

   A can contain Vars, not so for assume!*)
 fun trivial (Cterm {thy_ref, t =A, T, maxidx, sorts}) =
   if T <> propT then
     raise THM ("trivial: the term must have type prop", 0, [])
   else
-    Thm (deriv_rule0 (Pt.AbsP ("H", NONE, Pt.PBound 0)),
+    Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx,
       shyps = sorts,
       hyps = [],

     val thy = Theory.deref thy_ref;
     val c = Sign.certify_class thy raw_c;
     val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c));
   in
     if Sign.of_sort thy (T, [c]) then
-      Thm (deriv_rule0 (Pt.OfClass (T, c)),
+      Thm (deriv_rule0 (Proofterm.OfClass (T, c)),
        {thy_ref = Theory.check_thy thy,
         tags = [],
         maxidx = maxidx,
         shyps = sorts,
         hyps = [],

         val witnessed = Sign.witness_sorts thy present extra;
         val extra' = fold (Sorts.remove_sort o #2) witnessed extra
           |> Sorts.minimal_sorts algebra;
         val shyps' = fold (Sorts.insert_sort o #2) present extra';
       in
-        Thm (deriv_rule_unconditional (Pt.strip_shyps_proof algebra present witnessed extra') der,
+        Thm (deriv_rule_unconditional
+          (Proofterm.strip_shyps_proof algebra present witnessed extra') der,
          {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
           shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
       end;
 
 (*Internalize sort constraints of type variables*)

     val tfrees = rev (Term.add_tfree_names prop []);
     val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
 
     val ps = map (apsnd (Future.map proof_body_of)) promises;
     val thy = Theory.deref thy_ref;
-    val (pthm as (_, (_, prop', _)), proof) = Pt.unconstrain_thm_proof thy shyps prop ps body;
+    val (pthm as (_, (_, prop', _)), proof) =
+      Proofterm.unconstrain_thm_proof thy shyps prop ps body;
     val der' = make_deriv [] [] [pthm] proof;
     val _ = Theory.check_thy thy;
   in
     Thm (der',
      {thy_ref = thy_ref,

     val tfrees = fold Term.add_tfrees hyps fixed;
     val prop1 = attach_tpairs tpairs prop;
     val (al, prop2) = Type.varify_global tfrees prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
-    (al, Thm (deriv_rule1 (Pt.varify_proof prop tfrees) der,
+    (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der,
      {thy_ref = thy_ref,
       tags = [],
       maxidx = Int.max (0, maxidx),
       shyps = shyps,
       hyps = hyps,

   let
     val prop1 = attach_tpairs tpairs prop;
     val prop2 = Type.legacy_freeze prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
-    Thm (deriv_rule1 (Pt.legacy_freezeT prop1) der,
+    Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der,
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx_of_term prop2,
       shyps = shyps,
       hyps = hyps,

     val Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...}) = orule;
     val (As, B) = Logic.strip_horn prop;
   in
     if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, [])
     else
-      Thm (deriv_rule1 (Pt.lift_proof gprop inc prop) der,
+      Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der,
        {thy_ref = merge_thys1 goal orule,
         tags = [],
         maxidx = maxidx + inc,
         shyps = Sorts.union shyps sorts,  (*sic!*)
         hyps = hyps,

 
 fun incr_indexes i (thm as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
   if i < 0 then raise THM ("negative increment", 0, [thm])
   else if i = 0 then thm
   else
-    Thm (deriv_rule1 (Pt.incr_indexes i) der,
+    Thm (deriv_rule1 (Proofterm.incr_indexes i) der,
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx + i,
       shyps = shyps,
       hyps = hyps,

     val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
     val thy = Theory.deref thy_ref;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     fun newth n (env, tpairs) =
       Thm (deriv_rule1
-          ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
-            Pt.assumption_proof Bs Bi n) der,
+          ((if Envir.is_empty env then I else (Proofterm.norm_proof' env)) o
+            Proofterm.assumption_proof Bs Bi n) der,
        {tags = [],
         maxidx = Envir.maxidx_of env,
         shyps = Envir.insert_sorts env shyps,
         hyps = hyps,
         tpairs =

     val (_, asms, concl) = Logic.assum_problems (~1, Bi);
   in
     (case find_index (fn asm => Pattern.aeconv (asm, concl)) asms of
       ~1 => raise THM ("eq_assumption", 0, [state])
     | n =>
-        Thm (deriv_rule1 (Pt.assumption_proof Bs Bi (n + 1)) der,
+        Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der,
          {thy_ref = thy_ref,
           tags = [],
           maxidx = maxidx,
           shyps = shyps,
           hyps = hyps,

       else if 0 < m andalso m < n then
         let val (ps, qs) = chop m asms
         in list_all (params, Logic.list_implies (qs @ ps, concl)) end
       else raise THM ("rotate_rule", k, [state]);
   in
-    Thm (deriv_rule1 (Pt.rotate_proof Bs Bi m) der,
+    Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der,
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx,
       shyps = shyps,
       hyps = hyps,

       else if 0 < m andalso m < n_j then
         let val (ps, qs) = chop m moved_prems
         in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
       else raise THM ("permute_prems: k", k, [rl]);
   in
-    Thm (deriv_rule1 (Pt.permute_prems_proof prems j m) der,
+    Thm (deriv_rule1 (Proofterm.permute_prems_proof prems j m) der,
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx,
       shyps = shyps,
       hyps = hyps,

              end
            val th =
              Thm (deriv_rule2
                    ((if Envir.is_empty env then I
                      else if Envir.above env smax then
-                       (fn f => fn der => f (Pt.norm_proof' env der))
+                       (fn f => fn der => f (Proofterm.norm_proof' env der))
                      else
-                       curry op oo (Pt.norm_proof' env))
-                    (Pt.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
+                       curry op oo (Proofterm.norm_proof' env))
+                    (Proofterm.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
                 {tags = [],
                  maxidx = Envir.maxidx_of env,
                  shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps),
                  hyps = union_hyps rhyps shyps,
                  tpairs = ntpairs,

      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
      fun newAs(As0, n, dpairs, tpairs) =
        let val (As1, rder') =
          if not lifted then (As0, rder)
          else (map (rename_bvars(dpairs,tpairs,B)) As0,
-           deriv_rule1 (Pt.map_proof_terms
+           deriv_rule1 (Proofterm.map_proof_terms
              (rename_bvars (dpairs, tpairs, Bound 0)) I) rder);
        in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
           handle TERM _ =>
           raise THM("bicompose: 1st premise", 0, [orule])
        end;

 fun invoke_oracle thy_ref1 name oracle arg =
   let val Cterm {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = oracle arg in
     if T <> propT then
       raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
     else
-      let val (ora, prf) = Pt.oracle_proof name prop in
+      let val (ora, prf) = Proofterm.oracle_proof name prop in
         Thm (make_deriv [] [ora] [] prf,
          {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
           tags = [],
           maxidx = maxidx,
           shyps = sorts,