# HG changeset patch
# User berghofe
# Date 999267879 -7200
# Node ID 5cb3be5fbb4c9d01ea9989deb3350138563a50d6
# Parent  8d0c6543304875df6e03809e884b421ac44fa00f
Exported ml_reserved.

diff -r 8d0c65433048 -r 5cb3be5fbb4c src/Pure/Thy/thm_database.ML
--- 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;