--- a/src/Pure/Tools/codegen_data.ML Mon Nov 13 15:43:15 2006 +0100
+++ b/src/Pure/Tools/codegen_data.ML Mon Nov 13 15:43:16 2006 +0100
@@ -8,15 +8,14 @@
signature CODEGEN_DATA =
sig
- type lthms = thm list Susp.T;
- val lazy: (unit -> thm list) -> lthms
+ val lazy: (unit -> thm list) -> thm list Susp.T
val eval_always: bool ref
val add_func: thm -> theory -> theory
val add_func_legacy: thm -> theory -> theory
val del_func: thm -> theory -> theory
- val add_funcl: CodegenConsts.const * lthms -> theory -> theory
- val add_datatype: string * (((string * sort) list * (string * typ list) list) * lthms)
+ val add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory
+ val add_datatype: string * (((string * sort) list * (string * typ list) list) * thm list Susp.T)
-> theory -> theory
val del_datatype: string -> theory -> theory
val add_inline: thm -> theory -> theory
@@ -62,7 +61,6 @@
(** lazy theorems, certificate theorems **)
-type lthms = thm list Susp.T;
val eval_always = ref false;
fun lazy f = if !eval_always
@@ -243,7 +241,7 @@
(* pairs of (selected, deleted) function theorems *)
-type sdthms = lthms * thm list;
+type sdthms = thm list Susp.T * thm list;
fun add_drop_redundant thm thms =
let
@@ -343,7 +341,7 @@
datatype spec = Spec of {
funcs: sdthms Consttab.table,
dconstrs: string Consttab.table,
- dtyps: (((string * sort) list * (string * typ list) list) * lthms) Symtab.table
+ dtyps: (((string * sort) list * (string * typ list) list) * thm list Susp.T) Symtab.table
};
fun mk_spec ((funcs, dconstrs), dtyps) =
--- a/src/Pure/Tools/codegen_names.ML Mon Nov 13 15:43:15 2006 +0100
+++ b/src/Pure/Tools/codegen_names.ML Mon Nov 13 15:43:16 2006 +0100
@@ -107,20 +107,6 @@
let
val names_ref = CodeName.get thy
val (Names names) = ! names_ref;
- fun mk_unique used name =
- let
- fun mk_name 0 = name
- | mk_name i = name ^ "_" ^ string_of_int i
- fun find_name i =
- let
- val name = mk_name i
- in
- if used name
- then find_name (i+1)
- else name
- end;
- val name = find_name 0;
- in name end;
val tabs = get_tabs names;
fun declare name =
let
@@ -129,11 +115,11 @@
in (names_ref := names'; name) end;
in case get (fst tabs) x
of SOME name => name
- | NONE => let
- val used = Symtab.defined (snd tabs);
- val raw_name = policy thy x;
- val name = mk_unique used raw_name;
- in declare name end
+ | NONE =>
+ x
+ |> policy thy
+ |> Name.variant (Symtab.keys (snd tabs))
+ |> declare
end;