src/Pure/thm.ML

     string list -> bool -> string * typ -> cterm * (indexname * typ) list
 
   (*theories*)
 
   (*proof terms [must duplicate declaration as a specification]*)
-  val full_deriv	: bool ref
+  datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
+  val keep_derivs	: deriv_kind ref
   datatype rule = 
       MinProof				
+    | Oracle of theory * Sign.sg * exn
     | Axiom		of theory * string
-    | Theorem		of theory * string	
+    | Theorem		of string	
     | Assume		of cterm
     | Implies_intr	of cterm
     | Implies_intr_shyps
     | Implies_intr_hyps
     | Implies_elim 

     | RewriteC		of cterm
     | CongC		of cterm
     | Rewrite_cterm	of cterm
     | Rename_params_rule of string list * int;
 
-  datatype deriv = Infer  of rule * deriv list
-		 | Oracle of theory * Sign.sg * exn;
+  type deriv   (* = rule mtree *)
 
   (*meta theorems*)
   type thm
   exception THM of string * int * thm list
   val rep_thm           : thm -> {sign: Sign.sg, der: deriv, maxidx: int,

   val extra_shyps       : thm -> sort list
   val force_strip_shyps : bool ref      (* FIXME tmp *)
   val strip_shyps       : thm -> thm
   val implies_intr_shyps: thm -> thm
   val get_axiom         : theory -> string -> thm
-  val name_thm          : theory * string * thm -> thm
+  val name_thm          : string * thm -> thm
   val axioms_of         : theory -> (string * thm) list
 
   (*meta rules*)
   val assume            : cterm -> thm
   val compress          : thm -> thm

 
 (*Names of rules in derivations.  Includes logically trivial rules, if 
   executed in ML.*)
 datatype rule = 
     MinProof				(*for building minimal proof terms*)
+  | Oracle   	        of theory * Sign.sg * exn	(*oracles*)
 (*Axioms/theorems*)
   | Axiom		of theory * string
-  | Theorem		of theory * string	(*via theorem db*)
+  | Theorem		of string
 (*primitive inferences and compound versions of them*)
   | Assume		of cterm
   | Implies_intr	of cterm
   | Implies_intr_shyps
   | Implies_intr_hyps

   | Rewrite_cterm	of cterm
 (*Logical identities, recorded since they are part of the proof process*)
   | Rename_params_rule	of string list * int;
 
 
-datatype deriv = Infer	of rule * deriv list
-	       | Oracle	of theory * Sign.sg * exn;
-
-
-val full_deriv = ref false;
-
-
-(*Suppress all atomic inferences, if using minimal derivations*)
-fun squash_derivs (Infer (_, []) :: drvs) =        squash_derivs drvs
-  | squash_derivs (der :: ders)           = der :: squash_derivs ders
-  | squash_derivs []                      = [];
+type deriv = rule mtree;
+
+datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
+
+val keep_derivs = ref MinDeriv;
+
+
+(*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) =
+     (case der of
+	  Join (Oracle _, _) => der :: squash_derivs ders
+	| Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 
+				      then der :: squash_derivs ders
+				      else squash_derivs (der'::ders)
+	| Join (Axiom _, _) => if !keep_derivs=ThmDeriv 
+			       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 = Infer (MinProof, []);
+val min_infer = Join (MinProof, []);
 
 (*Make a minimal inference*)
 fun make_min_infer []    = min_infer
   | make_min_infer [der] = der
-  | make_min_infer ders  = Infer (MinProof, ders);
-
-fun infer_derivs (rl, [])   = Infer (rl, [])
+  | make_min_infer ders  = Join (MinProof, ders);
+
+fun infer_derivs (rl, [])   = Join (rl, [])
   | infer_derivs (rl, ders) =
-    if !full_deriv then Infer (rl, ders)
+    if !keep_derivs=FullDeriv then Join (rl, ders)
     else make_min_infer (squash_derivs ders);
 
 
 (*** Meta theorems ***)
 

 
 (*errors involving theorems*)
 exception THM of string * int * thm list;
 
 
-val sign_of_thm = #sign o rep_thm;
-val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm;
+val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm;
 
 (*merge signatures of two theorems; raise exception if incompatible*)
 fun merge_thm_sgs (th1, th2) =
-  Sign.merge (pairself sign_of_thm (th1, th2))
+  Sign.merge (pairself (#sign o rep_thm) (th1, th2))
     handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
 
 
 (*maps object-rule to tpairs*)
 fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);

 (*return additional axioms of this theory node*)
 fun axioms_of thy =
   map (fn (s, _) => (s, get_axiom thy s))
     (Symtab.dest (#new_axioms (rep_theory thy)));
 
-fun name_thm (thy, name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = 
-    if Sign.eq_sg (sign, sign_of thy) then
-	Thm {sign = sign, 
-	     der = Infer (Theorem(thy,name), [der]),
-	     maxidx = maxidx,
-	     shyps = shyps, 
-	     hyps = hyps, 
-	     prop = prop}
-    else raise THM ("name_thm", 0, [th]);
+(*Attach a label to a theorem to make proof objects more readable*)
+fun name_thm (name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = 
+    Thm {sign = sign, 
+	 der = Join (Theorem name, [der]),
+	 maxidx = maxidx,
+	 shyps = shyps, 
+	 hyps = hyps, 
+	 prop = prop};
 
 
 (*Compression of theorems -- a separate rule, not integrated with the others,
   as it could be slow.*)
 fun compress (Thm {sign, der, maxidx, shyps, hyps, prop}) = 

 (* Equality *)
 
 (* Definition of the relation =?= *)
 val flexpair_def = fix_shyps [] []
   (Thm{sign= Sign.proto_pure, 
-       der = Infer(Axiom(pure_thy, "flexpair_def"), []),
+       der = Join(Axiom(pure_thy, "flexpair_def"), []),
        shyps = [], 
        hyps = [], 
        maxidx = 0,
        prop = term_of (read_cterm Sign.proto_pure
 		       ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))});

 		    Sign.certify_term sign' (oracle (sign', exn))
             in if T<>propT then
                   raise THM("Oracle's result must have type prop", 0, [])
 	       else fix_shyps [] []
 		     (Thm {sign = sign', 
-			   der = Oracle(thy,sign,exn),
+			   der = Join (Oracle(thy,sign,exn), []),
 			   maxidx = maxidx,
 			   shyps = [], 
 			   hyps = [], 
 			   prop = prop})
             end;