# HG changeset patch
# User wenzelm
# Date 1206567718 -3600
# Node ID 945d8d7a66ec82c14b8aa1e69130a254a5cf2b26
# Parent  02709831944abbd32a6982d73df10b158b89a882
removed obsolete Thy/thm_database.ML (cf. ML/ml_context.ML);

diff -r 02709831944a -r 945d8d7a66ec src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Mar 26 22:40:10 2008 +0100
+++ b/src/Pure/IsaMakefile	Wed Mar 26 22:41:58 2008 +0100
@@ -67,9 +67,9 @@
   Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
   Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML		\
   Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML	\
-  Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_database.ML	\
-  Thy/thm_deps.ML Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML	\
-  Thy/thy_load.ML Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML	\
+  Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML		\
+  Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML	\
+  Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML			\
   Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML	\
   assumption.ML axclass.ML codegen.ML compress.ML config.ML		\
   conjunction.ML consts.ML context.ML conv.ML defs.ML display.ML	\
diff -r 02709831944a -r 945d8d7a66ec src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Wed Mar 26 22:40:10 2008 +0100
+++ b/src/Pure/Isar/ROOT.ML	Wed Mar 26 22:41:58 2008 +0100
@@ -29,7 +29,6 @@
 use "../Thy/present.ML";
 use "../Thy/thy_info.ML";
 use "../Thy/thm_deps.ML";
-use "../Thy/thm_database.ML";
 
 (*basic proof engine*)
 use "proof_display.ML";
diff -r 02709831944a -r 945d8d7a66ec src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Wed Mar 26 22:40:10 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-(*  Title:      Pure/Thy/thm_database.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-ML toplevel interface to the theorem database.
-*)
-
-signature BASIC_THM_DATABASE =
-sig
-  val store_thm: string * thm -> thm
-  val store_thms: string * thm list -> thm list
-end;
-
-signature THM_DATABASE =
-sig
-  include BASIC_THM_DATABASE
-  val qed_thms: thm list ref
-  val ml_store_thm: string * thm -> unit
-  val ml_store_thms: string * thm list -> unit
-end;
-
-structure ThmDatabase: THM_DATABASE =
-struct
-
-(** store theorems **)
-
-(* store in theory and perform presentation *)
-
-fun store_thm (name, thm) =
-  let val thm' = hd (PureThy.smart_store_thms (name, [thm]))
-  in Present.theorem name thm'; thm' end;
-
-fun store_thms (name, thms) =
-  let val thms' = PureThy.smart_store_thms (name, thms)
-  in Present.theorems name thms'; thms' end;
-
-
-(* store on ML toplevel *)
-
-val qed_thms: thm list ref = ref [];
-
-fun warn_ml name =
-  if ML_Syntax.is_identifier name then false
-  else if name = "" then true
-  else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
-
-val use_text_verbose = use_text (0, "") Output.ml_output true;
-
-fun ml_store_thm (name, thm) =
-  let val thm' = store_thm (name, thm) in
-    if warn_ml name then ()
-    else NAMED_CRITICAL "ML" (fn () => (qed_thms := [thm'];
-      use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")))
-  end;
-
-fun ml_store_thms (name, thms) =
-  let val thms' = store_thms (name, thms) in
-    if warn_ml name then ()
-    else NAMED_CRITICAL "ML" (fn () => (qed_thms := thms';
-      use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")))
-  end;
-
-end;
-
-structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
-open BasicThmDatabase;