explicit type arguments in constants

--- a/src/Tools/code/code_haskell.ML	Wed May 06 16:01:06 2009 +0200
+++ b/src/Tools/code/code_haskell.ML	Wed May 06 16:01:06 2009 +0200
@@ -261,7 +261,7 @@
                     val vars = init_syms
                       |> Code_Printer.intro_vars (the_list const)
                       |> Code_Printer.intro_vars vs;
-                    val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs;
+                    val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
                       (*dictionaries are not relevant at this late stage*)
                   in
                     semicolon [

--- a/src/Tools/code/code_ml.ML	Wed May 06 16:01:06 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Wed May 06 16:01:06 2009 +0200
@@ -109,7 +109,7 @@
                 then pr_case is_closure thm vars fxy cases
                 else pr_app is_closure thm vars fxy c_ts
             | NONE => pr_case is_closure thm vars fxy cases)
-    and pr_app' is_closure thm vars (app as ((c, (iss, tys)), ts)) =
+    and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) =
       if is_cons c then
         let
           val k = length tys
@@ -414,7 +414,7 @@
                 then pr_case is_closure thm vars fxy cases
                 else pr_app is_closure thm vars fxy c_ts
             | NONE => pr_case is_closure thm vars fxy cases)
-    and pr_app' is_closure thm vars (app as ((c, (iss, tys)), ts)) =
+    and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) =
       if is_cons c then
         if length tys = length ts
         then case ts

--- a/src/Tools/code/code_thingol.ML	Wed May 06 16:01:06 2009 +0200
+++ b/src/Tools/code/code_thingol.ML	Wed May 06 16:01:06 2009 +0200
@@ -20,7 +20,7 @@
   datatype itype =
       `%% of string * itype list
     | ITyVar of vname;
-  type const = string * (dict list list * itype list (*types of arguments*))
+  type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
   datatype iterm =
       IConst of const
     | IVar of vname
@@ -44,11 +44,10 @@
   val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm
   val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
-  val unfold_const_app: iterm ->
-    ((string * (dict list list * itype list)) * iterm list) option
+  val unfold_const_app: iterm -> (const * iterm list) option
   val collapse_let: ((vname * itype) * iterm) * iterm
     -> (iterm * itype) * (iterm * iterm) list
-  val eta_expand: int -> (string * (dict list list * itype list)) * iterm list -> iterm
+  val eta_expand: int -> const * iterm list -> iterm
   val contains_dictvar: iterm -> bool
   val locally_monomorphic: iterm -> bool
   val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
@@ -122,7 +121,7 @@
     `%% of string * itype list
   | ITyVar of vname;
 
-type const = string * (dict list list * itype list (*types of arguments*))
+type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
 
 datatype iterm =
     IConst of const
@@ -212,7 +211,7 @@
       | contains (DictVar _) = K true;
   in
     fold_aiterms
-      (fn IConst (_, (dss, _)) => (fold o fold) contains dss | _ => I) t false
+      (fn IConst (_, ((_, dss), _)) => (fold o fold) contains dss | _ => I) t false
   end;
   
 fun locally_monomorphic (IConst _) = false
@@ -602,9 +601,10 @@
     val tys_args = (fst o Term.strip_type) ty;
   in
     ensure_const thy algbr funcgr c
+    ##>> fold_map (translate_typ thy algbr funcgr) tys
     ##>> fold_map (translate_dicts thy algbr funcgr thm) (tys ~~ sorts)
     ##>> fold_map (translate_typ thy algbr funcgr) tys_args
-    #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
+    #>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args)))
   end
 and translate_app_const thy algbr funcgr thm (c_ty, ts) =
   translate_const thy algbr funcgr thm c_ty

--- a/src/Tools/nbe.ML	Wed May 06 16:01:06 2009 +0200
+++ b/src/Tools/nbe.ML	Wed May 06 16:01:06 2009 +0200
@@ -194,7 +194,7 @@
           let
             val (t', ts) = Code_Thingol.unfold_app t
           in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
-        and of_iapp match_cont (IConst (c, (dss, _))) ts = constapp c dss ts
+        and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
           | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
           | of_iapp match_cont ((v, _) `|-> t) ts =
               nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts
@@ -299,15 +299,15 @@
         val params = Name.invent_list [] "d" (length names);
         fun mk (k, name) =
           (name, ([(v, [])],
-            [([IConst (class, ([], [])) `$$ map IVar params], IVar (nth params k))]));
+            [([IConst (class, (([], []), [])) `$$ map IVar params], IVar (nth params k))]));
       in map_index mk names end
   | eqns_of_stmt (_, Code_Thingol.Classrel _) =
       []
   | eqns_of_stmt (_, Code_Thingol.Classparam _) =
       []
   | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
-      [(inst, (arities, [([], IConst (class, ([], [])) `$$
-        map (fn (_, (_, (inst, dicts))) => IConst (inst, (dicts, []))) superinsts
+      [(inst, (arities, [([], IConst (class, (([], []), [])) `$$
+        map (fn (_, (_, (inst, dicts))) => IConst (inst, (([], dicts), []))) superinsts
         @ map (IConst o snd o fst) instops)]))];
 
 fun compile_stmts ctxt stmts_deps =