# HG changeset patch
# User wenzelm
# Date 1125237894 -7200
# Node ID cbe14eb12729233394c9fdfefb5dc172ea614309
# Parent  1f12d55060bff08028f39aafe5aa9ad91caa47dd
added (use_)legacy_bindings;

diff -r 1f12d55060bf -r cbe14eb12729 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Sun Aug 28 16:04:53 2005 +0200
+++ b/src/Pure/Thy/thm_database.ML	Sun Aug 28 16:04:54 2005 +0200
@@ -2,13 +2,15 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Theorem database ML interface.
+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
+  val legacy_bindings: theory -> string
+  val use_legacy_bindings: theory -> unit
 end;
 
 signature THM_DATABASE =
@@ -73,6 +75,44 @@
   end;
 
 
+(* legacy bindings *)
+
+fun legacy_bindings thy =
+  let
+    val thy_name = Context.theory_name thy;
+    val (space, thms) = PureThy.theorems_of thy;
+
+    fun prune name =
+      let
+        val xname = NameSpace.extern space name;
+        fun result prfx bname =
+          if (prfx = "" orelse is_ml_identifier prfx) andalso is_ml_identifier bname andalso
+              NameSpace.intern space xname = name then
+            SOME (prfx, (bname, xname, length (the (Symtab.lookup (thms, name))) = 1))
+          else NONE;
+        val names = NameSpace.unpack name;
+      in
+        (case #2 (splitAt (length names - 2, names)) of
+          [bname] => result "" bname
+        | [prfx, bname] => result (if prfx = thy_name then "" else prfx) bname
+        | _ => NONE)
+      end;
+
+    fun mk_struct "" = I
+      | mk_struct prfx = enclose ("structure " ^ prfx ^ " =\nstruct\n") "\nend\n";
+
+    fun mk_thm (bname, xname, singleton) =
+      "val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname;
+  in
+    Symtab.keys thms |> List.mapPartial prune
+    |> Symtab.make_multi |> Symtab.dest |> sort_wrt #1
+    |> map (fn (prfx, entries) =>
+      entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx)
+    |> cat_lines
+  end;
+
+fun use_legacy_bindings thy = Context.use_mltext (legacy_bindings thy) true (SOME thy);
+
 end;
 
 structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;