removed deriv.ML which is now incorporated into thm.ML;

--- a/src/Pure/IsaMakefile	Mon Sep 22 15:26:11 2008 +0200
+++ b/src/Pure/IsaMakefile	Mon Sep 22 15:26:11 2008 +0200
@@ -76,14 +76,13 @@
   Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML Tools/quickcheck.ML	\
   Tools/value.ML Tools/isabelle_process.ML Tools/named_thms.ML		\
   Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
-  conjunction.ML consts.ML context.ML conv.ML defs.ML deriv.ML		\
-  display.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML	\
-  library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML	\
-  name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML		\
-  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML		\
-  simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML	\
-  term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML		\
-  variable.ML
+  conjunction.ML consts.ML context.ML conv.ML defs.ML display.ML	\
+  drule.ML envir.ML facts.ML goal.ML interpretation.ML library.ML	\
+  logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML	\
+  old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML	\
+  pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML	\
+  tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML	\
+  type_infer.ML unify.ML variable.ML
 	@./mk
 
 

--- a/src/Pure/ROOT.ML	Mon Sep 22 15:26:11 2008 +0200
+++ b/src/Pure/ROOT.ML	Mon Sep 22 15:26:11 2008 +0200
@@ -61,7 +61,6 @@
 use "theory.ML";
 use "interpretation.ML";
 use "proofterm.ML";
-use "deriv.ML";
 use "thm.ML";
 use "more_thm.ML";
 use "facts.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;