diff -r 83c4fc383409 -r 6b8d001ce1de src/Pure/deriv.ML
--- a/src/Pure/deriv.ML	Mon Sep 22 15:26:11 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(*  Title:      Pure/deriv.ML
-    ID:         $Id$
-    Author:     Makarius
-
-Abstract derivations based on raw proof terms.
-*)
-
-signature DERIV =
-sig
-  type T
-  val oracle_of: T -> bool
-  val proof_of: T -> Proofterm.proof
-  val uncond_rule: (Proofterm.proof -> Proofterm.proof) -> T -> T
-  val rule0: Proofterm.proof -> T
-  val rule1: (Proofterm.proof -> Proofterm.proof) -> T -> T
-  val rule2: (Proofterm.proof -> Proofterm.proof -> Proofterm.proof) -> T -> T -> T
-  val oracle: string -> term -> T
-end;
-
-structure Deriv: DERIV =
-struct
-
-datatype T = Der of bool * Proofterm.proof;
-
-fun oracle_of (Der (ora, _)) = ora;
-fun proof_of (Der (_, proof)) = proof;
-
-fun uncond_rule f (Der (ora, prf)) = Der (ora, f prf);
-
-fun rule0 prf = Der (Proofterm.infer_derivs' I (false, prf));
-fun rule1 f (Der der) = Der (Proofterm.infer_derivs' f der);
-fun rule2 f (Der der1) (Der der2) = Der (Proofterm.infer_derivs f der1 der2);
-
-fun oracle name prop = Der (true, Proofterm.oracle_proof name prop);
-
-end;