Exported ml_reserved.

--- a/src/Pure/Thy/thm_database.ML	Fri Aug 31 16:24:00 2001 +0200
+++ b/src/Pure/Thy/thm_database.ML	Fri Aug 31 16:24:39 2001 +0200
@@ -29,6 +29,7 @@
   val ml_store_thm: string * thm -> unit
   val ml_store_thms: string * thm list -> unit
   val is_ml_identifier: string -> bool
+  val ml_reserved: string list
   val print_thms_containing: theory -> term list -> unit
 end;