ML runtime compilation: pass position, tuned signature;
authorwenzelm
Mon Mar 24 23:34:30 2008 +0100 (2008-03-24 ago)
changeset 263869c806de22a6a
parent 26385 ae7564661e76
child 26387 7807cbf7640f
ML runtime compilation: pass position, tuned signature;
removed obsolete (use_)legacy_bindings;
src/Pure/Thy/thm_database.ML
     1.1 --- a/src/Pure/Thy/thm_database.ML	Mon Mar 24 23:34:24 2008 +0100
     1.2 +++ b/src/Pure/Thy/thm_database.ML	Mon Mar 24 23:34:30 2008 +0100
     1.3 @@ -9,8 +9,6 @@
     1.4  sig
     1.5    val store_thm: string * thm -> thm
     1.6    val store_thms: string * thm list -> thm list
     1.7 -  val legacy_bindings: theory -> string
     1.8 -  val use_legacy_bindings: theory -> unit
     1.9  end;
    1.10  
    1.11  signature THM_DATABASE =
    1.12 @@ -46,7 +44,7 @@
    1.13    else if name = "" then true
    1.14    else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
    1.15  
    1.16 -val use_text_verbose = use_text "" Output.ml_output true;
    1.17 +val use_text_verbose = use_text (0, "") Output.ml_output true;
    1.18  
    1.19  fun ml_store_thm (name, thm) =
    1.20    let val thm' = store_thm (name, thm) in
    1.21 @@ -62,47 +60,6 @@
    1.22        use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")))
    1.23    end;
    1.24  
    1.25 -
    1.26 -(* legacy bindings *)
    1.27 -
    1.28 -fun legacy_bindings thy =
    1.29 -  let
    1.30 -    val thy_name = Context.theory_name thy;
    1.31 -    val (space, thms) = PureThy.theorems_of thy;
    1.32 -
    1.33 -    fun prune name =
    1.34 -      let
    1.35 -        val xname = NameSpace.extern space name;
    1.36 -        fun result prfx bname =
    1.37 -          if (prfx = "" orelse ML_Syntax.is_identifier prfx) andalso
    1.38 -              ML_Syntax.is_identifier bname andalso
    1.39 -              NameSpace.intern space xname = name then
    1.40 -            SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1))
    1.41 -          else NONE;
    1.42 -        val names = NameSpace.explode name;
    1.43 -      in
    1.44 -        (case #2 (chop (length names - 2) names) of
    1.45 -          [bname] => result "" bname
    1.46 -        | [prfx, bname] => result (if prfx = thy_name then "" else prfx) bname
    1.47 -        | _ => NONE)
    1.48 -      end;
    1.49 -
    1.50 -    fun mk_struct "" = I
    1.51 -      | mk_struct prfx = enclose ("structure " ^ prfx ^ " =\nstruct\n") "\nend\n";
    1.52 -
    1.53 -    fun mk_thm (bname, xname, singleton) =
    1.54 -      "val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname;
    1.55 -  in
    1.56 -    Symtab.keys thms |> map_filter prune
    1.57 -    |> Symtab.make_list |> Symtab.dest |> sort_wrt #1
    1.58 -    |> map (fn (prfx, entries) =>
    1.59 -      entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx)
    1.60 -    |> cat_lines
    1.61 -  end;
    1.62 -
    1.63 -fun use_legacy_bindings thy =
    1.64 -  ML_Context.use_mltext (legacy_bindings thy) true (SOME (Context.Theory thy));
    1.65 -
    1.66  end;
    1.67  
    1.68  structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;