removed obsolete Thy/thm_database.ML (cf. ML/ml_context.ML);
--- 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 \
--- 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";
--- 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;