src/Pure/thm.ML

     | Rename_params_rule  of string list * int;
   type deriv	(* = rule mtree *)
 
   (*meta theorems*)
   type thm
-  val rep_thm           : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
+  val rep_thm           : thm -> {sign: Sign.sg, der: bool * deriv, maxidx: int,
                                   shyps: sort list, hyps: term list, 
                                   prop: term}
-  val crep_thm          : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
+  val crep_thm          : thm -> {sign: Sign.sg, der: bool * deriv, maxidx: int,
                                   shyps: sort list, hyps: cterm list, 
                                   prop: cterm}
   exception THM of string * int * thm list
   type 'a attribute 	(* = 'a * thm -> 'a * thm *)
   val eq_thm		: thm * thm -> bool

 
 datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
 
 val keep_derivs = ref MinDeriv;
 
+local
 
 (*Build a minimal derivation.  Keep oracles; suppress atomic inferences;
   retain Theorems or their underlying links; keep anything else*)
 fun squash_derivs [] = []
   | squash_derivs (der::ders) =

                                then der :: squash_derivs ders
                                else squash_derivs ders
         | Join (_, [])      => squash_derivs ders
         | _                 => der :: squash_derivs ders);
 
-
 (*Ensure sharing of the most likely derivation, the empty one!*)
 val min_infer = Join (MinProof, []);
 
 (*Make a minimal inference*)
 fun make_min_infer []    = min_infer
   | make_min_infer [der] = der
   | make_min_infer ders  = Join (MinProof, ders);
 
-fun infer_derivs (rl, [])   = Join (rl, [])
+fun is_oracle (Oracle _) = true
+  | is_oracle _ = false;
+
+in
+
+fun infer_derivs (rl, []: (bool * deriv) list)   = (is_oracle rl, Join (rl, []))
   | infer_derivs (rl, ders) =
-    if !keep_derivs=FullDeriv then Join (rl, ders)
-    else make_min_infer (squash_derivs ders);
+      (is_oracle rl orelse exists #1 ders,
+        if !keep_derivs=FullDeriv then Join (rl, map #2 ders)
+        else make_min_infer (squash_derivs (map #2 ders)));
+
+end;
 
 
 
 (*** Meta theorems ***)
 
 datatype thm = Thm of
  {sign_ref: Sign.sg_ref,       (*mutable reference to signature*)
-  der: deriv,                  (*derivation*)
+  der: bool * deriv,           (*derivation*)
   maxidx: int,                 (*maximum index of any Var or TVar*)
   shyps: sort list,            (*sort hypotheses*)
   hyps: term list,             (*hypotheses*)
   prop: term};                 (*conclusion*)
 

 
 
 (* name and tags -- make proof objects more readable *)
 
 fun get_name_tags (Thm {der, ...}) =
-  (case der of
+  (case #2 der of
     Join (Theorem x, _) => x
   | Join (Axiom x, _) => x
   | _ => ("", []));
 
-fun put_name_tags x (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
+fun put_name_tags x (Thm {sign_ref, der = (ora, der), maxidx, shyps, hyps, prop}) =
   let
     val der' =
       (case der of
         Join (Theorem _, ds) => Join (Theorem x, ds)
       | Join (Axiom _, ds) => Join (Axiom x, ds)
       | _ => Join (Theorem x, [der]));
   in
-    Thm {sign_ref = sign_ref, der = der', maxidx = maxidx,
+    Thm {sign_ref = sign_ref, der = (ora, der'), maxidx = maxidx,
       shyps = shyps, hyps = hyps, prop = prop}
   end;
 
 val name_of_thm = #1 o get_name_tags;
 val tags_of_thm = #2 o get_name_tags;

           (case botc true skel0 mss trec of
              Some(trec1) => trec1 | None => trec)
 
     and subc skel
              (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless})
-             (trec as (t0:term,etc:sort list*term list * rule mtree list)) =
+             (trec as (t0:term,etc:sort list*term list * (bool * deriv) list)) =
        (case t0 of
            Abs(a,T,t) =>
              let val b = variant bounds a
                  val v = Free("." ^ b,T)
                  val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)

       in
         if T <> propT then
           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
         else fix_shyps [] []
           (Thm {sign_ref = sign_ref', 
-            der = Join (Oracle (name, sign, exn), []),
+            der = (true, Join (Oracle (name, sign, exn), [])),
             maxidx = maxidx,
             shyps = [], 
             hyps = [], 
             prop = prop})
       end