# HG changeset patch
# User haftmann
# Date 1163428996 -3600
# Node ID 56d55dd30311159b6953a7a35aa3cc2454de7966
# Parent  d89d2cb8a05fc710df29e25145076ae39b061335
cleaned up

diff -r d89d2cb8a05f -r 56d55dd30311 src/Pure/Tools/codegen_data.ML
--- 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) =
diff -r d89d2cb8a05f -r 56d55dd30311 src/Pure/Tools/codegen_names.ML
--- 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;