# HG changeset patch
# User haftmann
# Date 1135180857 -3600
# Node ID b293c1087f1dddf47d5b2a4189f2470f61da5b3f
# Parent  6720b5010a57077fc56404123448fdd4dd5f36df
slight improvements

diff -r 6720b5010a57 -r b293c1087f1d src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Dec 21 15:19:16 2005 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Dec 21 17:00:57 2005 +0100
@@ -70,7 +70,7 @@
   val get_datatype : theory -> string -> ((string * sort) list * string list) option
   val get_datatype_cons : theory -> string * string -> typ list option
   val get_case_const_data : theory -> string -> (string * int) list option
-  val get_all_datatype_cons : theory -> (string * string list) list
+  val get_all_datatype_cons : theory -> (string * string) list
   val constrs_of : theory -> string -> term list option
   val case_const_of : theory -> string -> term option
   val weak_case_congs_of : theory -> thm list
@@ -1003,9 +1003,9 @@
 
 fun get_all_datatype_cons thy =
   Symtab.fold (fn (dtco, _) => fold
-    (fn co =>
-      AList.default (op =) (co, []) #> AList.map_entry (op =) co (cons dtco))
-    ((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) [];
+    (fn co => cons (co, dtco))
+      ((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) [];
+
 
 
 (** package setup **)
diff -r 6720b5010a57 -r b293c1087f1d src/Pure/General/name_mangler.ML
--- a/src/Pure/General/name_mangler.ML	Wed Dec 21 15:19:16 2005 +0100
+++ b/src/Pure/General/name_mangler.ML	Wed Dec 21 17:00:57 2005 +0100
@@ -89,8 +89,12 @@
           fun mk_it (seed, i) =
             let
               val name = mk ctxt (seed, i)
-            in if is_valid ctxt name then name
-            else mk_it (seed, i+1) end;
+            in
+              if is_valid ctxt name
+                andalso (not oo Symtab.defined) tab_r name
+              then name 
+              else mk_it (seed, i+1)
+            end;
           val name = (fst oooo mk_unique) (op =) mk_it x [];
         in
           (name,
@@ -110,8 +114,12 @@
         fun mk_it (seed, i) =
           let
             val name = mk ctxt (seed, i)
-          in if is_valid ctxt name then name
-          else mk_it (seed, i+1) end;
+          in
+            if is_valid ctxt name
+              andalso (not oo Symtab.defined) tab_r name
+            then name
+            else mk_it (seed, i+1)
+          end;
         val names = (fst oooo mk_unique_multi) (op =) mk_it xs [];
       in
         (names,
diff -r 6720b5010a57 -r b293c1087f1d src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Dec 21 15:19:16 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Wed Dec 21 17:00:57 2005 +0100
@@ -33,7 +33,7 @@
     -> theory -> theory;
   val add_alias: string * string -> theory -> theory;
   val set_is_datatype: (theory -> string -> bool) -> theory -> theory;
-  val set_get_all_datatype_cons : (theory -> (string * string list) list)
+  val set_get_all_datatype_cons : (theory -> (string * string) list)
     -> theory -> theory;
 
   val invoke_cg_type: theory -> auxtab
@@ -161,6 +161,7 @@
     | mk thy ((co, dtco), i) =
         let
           fun basename 0 = NameSpace.base co
+            | basename 1 = NameSpace.base dtco ^ "_" ^ NameSpace.base co
             | basename i = NameSpace.base dtco ^ "_" ^ NameSpace.base co ^ "_" ^ (implode oo replicate) (i-1) "'";
           fun strip_dtco name =
             case (rev o NameSpace.unpack) name
@@ -254,7 +255,7 @@
 
 type logic_data = {
   is_datatype: ((theory -> string -> bool) * stamp) option,
-  get_all_datatype_cons: ((theory -> (string * string list) list) * stamp) option,
+  get_all_datatype_cons: ((theory -> (string * string) list) * stamp) option,
   alias: string Symtab.table * string Symtab.table
 };
 
@@ -594,7 +595,7 @@
         | _ => "";
     val c' = case Symtab.lookup overltab1 c
        of SOME (ty_decl, tys) => ConstNameMangler.get thy overltab2
-         (idf_of_name thy nsp_overl c, (ty_decl, (the oo find_first) (fn ty => Sign.typ_instance thy (ty, ty_decl)) tys))
+         (idf_of_name thy nsp_overl c, (ty_decl, (the oo find_first) (fn ty' => Sign.typ_instance thy (ty', ty)) tys))
         | NONE => case try (DatatypeconsNameMangler.get thy dtcontab) (c, coty)
        of SOME c' => idf_of_name thy nsp_dtcon c'
         | NONE => case Symtab.lookup clsmemtab c
@@ -1130,9 +1131,12 @@
     fun mk_dtcontab thy =
       DatatypeconsNameMangler.empty
       |> fold_map
-          (fn (co, dtcos) => DatatypeconsNameMangler.declare_multi thy
-              (map (pair co) dtcos))
-            (get_all_datatype_cons thy)
+          (fn (_, co_dtco) => DatatypeconsNameMangler.declare_multi thy co_dtco)
+            (fold (fn (co, dtco) =>
+              let
+                val key = ((NameSpace.drop_base o NameSpace.drop_base) co, NameSpace.base co)
+              in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end
+            ) (get_all_datatype_cons thy) [])
       |-> (fn _ => I);
     fun mk_deftab thy defs overltab =
       Symtab.empty
@@ -1491,12 +1495,8 @@
     add_alias ("op +", "HOL.op_add"),
     add_alias ("op -", "HOL.op_minus"),
     add_alias ("op *", "HOL.op_times"),
-(*     add_alias ("0", "Nat.Zero"),  *)
-    add_alias ("op <>", "HOL.op_neq"),
-    add_alias ("op >=", "op_ge"),
-    add_alias ("op >", "op_gt"),
-    add_alias ("op <=", "op_le"),
-    add_alias ("op <", "op_lt"),
+    add_alias ("op <=", "Orderings.op_le"),
+    add_alias ("op <", "Orderings.op_lt"),
     add_alias ("List.op @", "List.append"),
     add_alias ("List.op mem", "List.member"),
     add_alias ("Divides.op div", "Divides.div"),