# HG changeset patch
# User haftmann
# Date 1151661843 -7200
# Node ID 33da452f0abe8f0fa81c12423006b9b9d75c78b4
# Parent  88bbe97ed0b0ba5c70a94b812d53d7b54ddb71f9
slight refinements

diff -r 88bbe97ed0b0 -r 33da452f0abe src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Fri Jun 30 12:03:36 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Fri Jun 30 12:04:03 2006 +0200
@@ -12,7 +12,7 @@
   val is_dtcon: string -> bool;
   val consts_of_idfs: theory -> string list -> (string * typ) list;
   val idfs_of_consts: theory -> (string * typ) list -> string list;
-  val get_root_module: theory -> CodegenThingol.module;
+  val get_root_module: theory -> CodegenThingol.module * theory;
   val get_ml_fun_datatype: theory -> (string -> string)
     -> ((string * CodegenThingol.funn) list -> Pretty.T)
         * ((string * CodegenThingol.datatyp) list -> Pretty.T);
@@ -801,9 +801,9 @@
       trns
       |> exprgen_type thy tabs ty
       |-> (fn ty => pair (IVar v))
-  | exprgen_term thy tabs (Abs (abs as (_, ty, _))) trns =
+  | exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns =
       let
-        val (v, t) = Term.variant_abs abs
+        val (v, t) = Term.variant_abs (CodegenTheorems.proper_name raw_v, ty, raw_t);
       in
         trns
         |> exprgen_type thy tabs ty
@@ -1113,7 +1113,10 @@
 fun idfs_of_consts thy =
   map (idf_of_const thy (mk_tabs thy NONE));
 
-val get_root_module = (#modl o CodegenData.get);
+fun get_root_module thy =
+  thy
+  |> CodegenTheorems.notify_dirty
+  |> `(#modl o CodegenData.get);
 
 fun get_ml_fun_datatype thy resolv =
   let
diff -r 88bbe97ed0b0 -r 33da452f0abe src/Pure/Tools/codegen_theorems.ML
--- a/src/Pure/Tools/codegen_theorems.ML	Fri Jun 30 12:03:36 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML	Fri Jun 30 12:04:03 2006 +0200
@@ -600,7 +600,8 @@
     fun rewrite_rhs conv thm = (case (Drule.strip_comb o cprop_of) thm
      of (ct', [ct1, ct2]) => (case term_of ct'
          of Const ("==", _) =>
-              Thm.equal_elim (combination (combination (reflexive ct') (reflexive ct1)) (conv ct2)) thm
+              Thm.equal_elim (combination (combination (reflexive ct') (reflexive ct1))
+                (conv ct2)) thm
           | _ => raise ERROR "rewrite_rhs")
       | _ => raise ERROR "rewrite_rhs");
     fun unvarify thms =
diff -r 88bbe97ed0b0 -r 33da452f0abe src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Fri Jun 30 12:03:36 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Fri Jun 30 12:04:03 2006 +0200
@@ -17,8 +17,9 @@
 sig
   type vname = string;
   type sortcontext = ClassPackage.sortcontext;
-  datatype iclasslookup = Instance of string * iclasslookup list list
-                        | Lookup of class list * (string * int);
+  datatype iclasslookup =
+      Instance of string * iclasslookup list list
+    | Lookup of class list * (vname * int);
   datatype itype =
       `%% of string * itype list
     | `-> of itype * itype
@@ -28,7 +29,7 @@
     | IVar of vname
     | `$ of iexpr * iexpr
     | `|-> of (vname * itype) * iexpr
-    | INum of IntInf.int (*positive!*) * iexpr
+    | INum of IntInf.int (*non-negative!*) * iexpr
     | IChar of string (*length one!*) * iexpr
     | IAbs of ((iexpr * itype) * iexpr) * iexpr
         (* (((binding expression (ve), binding type (vty)),
@@ -153,8 +154,9 @@
 type vname = string;
 
 type sortcontext = ClassPackage.sortcontext;
-datatype iclasslookup = Instance of string * iclasslookup list list
-                      | Lookup of class list * (string * int);
+datatype iclasslookup =
+    Instance of string * iclasslookup list list
+  | Lookup of class list * (vname * int);
 
 datatype itype =
     `%% of string * itype list
@@ -166,7 +168,7 @@
   | IVar of vname
   | `$ of iexpr * iexpr
   | `|-> of (vname * itype) * iexpr
-  | INum of IntInf.int (*positive!*) * iexpr
+  | INum of IntInf.int (*non-negative!*) * iexpr
   | IChar of string (*length one!*) * iexpr
   | IAbs of ((iexpr * itype) * iexpr) * iexpr
   | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;