# 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;