ML runtime compilation: pass position, tuned signature;
removed obsolete (use_)legacy_bindings;

--- a/src/Pure/Thy/thm_database.ML	Mon Mar 24 23:34:24 2008 +0100
+++ b/src/Pure/Thy/thm_database.ML	Mon Mar 24 23:34:30 2008 +0100
@@ -9,8 +9,6 @@
 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 =
@@ -46,7 +44,7 @@
   else if name = "" then true
   else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
 
-val use_text_verbose = use_text "" Output.ml_output 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
@@ -62,47 +60,6 @@
       use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")))
   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 ML_Syntax.is_identifier prfx) andalso
-              ML_Syntax.is_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.explode name;
-      in
-        (case #2 (chop (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 |> map_filter prune
-    |> Symtab.make_list |> 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 =
-  ML_Context.use_mltext (legacy_bindings thy) true (SOME (Context.Theory thy));
-
 end;
 
 structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;