# HG changeset patch
# User haftmann
# Date 1338872756 -7200
# Node ID ace701efe203b4a6420b88a30696cc990fe308b2
# Parent  d7864276bca8938fba936cb155678da403567e66
prefer records with speaking labels over deeply nested tuples

diff -r d7864276bca8 -r ace701efe203 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 05 07:05:56 2012 +0200
@@ -633,8 +633,12 @@
     (*assumption: dummy values are not relevant for serialization*)
     val (unitt, unitT) = case lookup_const naming @{const_name Unity}
      of SOME unit' =>
-        let val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
-        in (IConst (unit', ((([], []), ([], unitT)), false)), unitT) end
+          let
+            val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
+          in
+            (IConst { name = unit', typargs = [], dicts = [], dom = [],
+              range = unitT, annotate = false }, unitT)
+          end
       | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
     fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
       | dest_abs (t, ty) =
@@ -643,21 +647,21 @@
             val v = singleton (Name.variant_list vs) "x";
             val ty' = (hd o fst o unfold_fun) ty;
           in ((SOME v, ty'), t `$ IVar (SOME v)) end;
-    fun force (t as IConst (c, _) `$ t') = if is_return c
+    fun force (t as IConst { name = c, ... } `$ t') = if is_return c
           then t' else t `$ unitt
       | force t = t `$ unitt;
     fun tr_bind'' [(t1, _), (t2, ty2)] =
       let
         val ((v, ty), t) = dest_abs (t2, ty2);
-      in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end
+      in ICase { term = force t1, typ = ty, clauses = [(IVar v, tr_bind' t)], primitive = dummy_case_term } end
     and tr_bind' t = case unfold_app t
-     of (IConst (c, ((_, (ty1 :: ty2 :: _, _)), _)), [x1, x2]) => if is_bind c
+     of (IConst { name = c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
           then tr_bind'' [(x1, ty1), (x2, ty2)]
           else force t
       | _ => force t;
-    fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
-      [(unitt, tr_bind'' ts)]), dummy_case_term)
-    fun imp_monad_bind' (const as (c, ((_, (tys, _)), _))) ts = if is_bind c then case (ts, tys)
+    fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=>
+      ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }
+    fun imp_monad_bind' (const as { name = c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
        of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
         | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
         | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
@@ -668,10 +672,9 @@
          of (IConst const, ts) => imp_monad_bind' const ts
           | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
       | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
-      | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
-          (((imp_monad_bind t, ty),
-            (map o pairself) imp_monad_bind pats),
-              imp_monad_bind t0);
+      | imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) =
+          ICase { term = imp_monad_bind t, typ = ty,
+            clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
 
   in (Graph.map o K o map_terms_stmt) imp_monad_bind end;
 
@@ -688,3 +691,4 @@
 hide_const (open) Heap heap guard raise' fold_map
 
 end
+
diff -r d7864276bca8 -r ace701efe203 src/HOL/Tools/list_code.ML
--- a/src/HOL/Tools/list_code.ML	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/HOL/Tools/list_code.ML	Tue Jun 05 07:05:56 2012 +0200
@@ -20,14 +20,14 @@
 
 fun implode_list nil' cons' t =
   let
-    fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
+    fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
           if c = cons'
           then SOME (t1, t2)
           else NONE
       | dest_cons _ = NONE;
     val (ts, t') = Code_Thingol.unfoldr dest_cons t;
   in case t'
-   of IConst (c, _) => if c = nil' then SOME ts else NONE
+   of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
     | _ => NONE
   end;
 
diff -r d7864276bca8 -r ace701efe203 src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/HOL/Tools/numeral.ML	Tue Jun 05 07:05:56 2012 +0200
@@ -69,11 +69,11 @@
   let
     fun dest_numeral one' bit0' bit1' thm t =
       let
-        fun dest_bit (IConst (c, _)) = if c = bit0' then 0
+        fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0
               else if c = bit1' then 1
               else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
           | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
-        fun dest_num (IConst (c, _)) = if c = one' then 1
+        fun dest_num (IConst { name = c, ... }) = if c = one' then 1
               else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
           | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
           | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
diff -r d7864276bca8 -r ace701efe203 src/HOL/Tools/string_code.ML
--- a/src/HOL/Tools/string_code.ML	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/HOL/Tools/string_code.ML	Tue Jun 05 07:05:56 2012 +0200
@@ -23,13 +23,13 @@
       | decode _ ~1 = NONE
       | decode n m = SOME (chr (n * 16 + m));
   in case tt
-   of (IConst (c1, _), IConst (c2, _)) => decode (idx c1) (idx c2)
+   of (IConst { name = c1, ... }, IConst { name = c2, ... }) => decode (idx c1) (idx c2)
     | _ => NONE
   end;
    
 fun implode_string char' nibbles' mk_char mk_string ts =
   let
-    fun implode_char (IConst (c, _) `$ t1 `$ t2) =
+    fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
           if c = char' then decode_char nibbles' (t1, t2) else NONE
       | implode_char _ = NONE;
     val ts' = map_filter implode_char ts;
diff -r d7864276bca8 -r ace701efe203 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Jun 05 07:05:56 2012 +0200
@@ -60,8 +60,8 @@
       print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
     fun print_typscheme tyvars (vs, ty) =
       Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
-    fun print_term tyvars some_thm vars fxy (IConst c) =
-          print_app tyvars some_thm vars fxy (c, [])
+    fun print_term tyvars some_thm vars fxy (IConst const) =
+          print_app tyvars some_thm vars fxy (const, [])
       | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
           (case Code_Thingol.unfold_const_app t
            of SOME app => print_app tyvars some_thm vars fxy app
@@ -79,15 +79,15 @@
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
             val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
           in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
-      | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
-          (case Code_Thingol.unfold_const_app t0
-           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
-                then print_case tyvars some_thm vars fxy cases
-                else print_app tyvars some_thm vars fxy c_ts
-            | NONE => print_case tyvars some_thm vars fxy cases)
-    and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
+      | print_term tyvars some_thm vars fxy (ICase case_expr) =
+          (case Code_Thingol.unfold_const_app (#primitive case_expr)
+           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+                then print_case tyvars some_thm vars fxy case_expr
+                else print_app tyvars some_thm vars fxy app
+            | NONE => print_case tyvars some_thm vars fxy case_expr)
+    and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
       let
-        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
+        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
         val printed_const =
           if annotate then
             brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
@@ -98,9 +98,11 @@
       end
     and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
     and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
-    and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
+    and print_case tyvars some_thm vars fxy { clauses = [], ... } =
+          (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
+      | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
           let
-            val (binds, body) = Code_Thingol.unfold_let (ICase cases);
+            val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
             fun print_match ((pat, _), t) vars =
               vars
               |> print_bind tyvars some_thm BR pat
@@ -110,7 +112,7 @@
             ps
             (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
           end
-      | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
+      | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
           let
             fun print_select (pat, body) =
               let
@@ -119,9 +121,7 @@
           in Pretty.block_enclose
             (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
             (map print_select clauses)
-          end
-      | print_case tyvars some_thm vars fxy ((_, []), _) =
-          (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
+          end;
     fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
@@ -221,7 +221,7 @@
               str "};"
             ) (map print_classparam classparams)
           end
-      | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
+      | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
             fun requires_args classparam = case const_syntax classparam
@@ -237,14 +237,15 @@
                     ]
                 | SOME k =>
                     let
-                      val (c, ((_, tys), _)) = const;
+                      val { name = c, dom, range, ... } = const;
                       val (vs, rhs) = (apfst o map) fst
                         (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
                       val s = if (is_some o const_syntax) c
                         then NONE else (SOME o Long_Name.base_name o deresolve) c;
                       val vars = reserved
                         |> intro_vars (map_filter I (s :: vs));
-                      val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
+                      val lhs = IConst { name = classparam, typargs = [],
+                        dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
                         (*dictionaries are not relevant at this late stage,
                           and these consts never need type annotations for disambiguation *)
                     in
@@ -264,7 +265,7 @@
                 str " where {"
               ],
               str "};"
-            ) (map print_classparam_instance classparam_instances)
+            ) (map print_classparam_instance inst_params)
           end;
   in print_stmt end;
 
@@ -407,7 +408,7 @@
      of SOME ((pat, ty), t') =>
           SOME ((SOME ((pat, ty), true), t1), t')
       | NONE => NONE;
-    fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
+    fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
           if c = c_bind_name then dest_bind t1 t2
           else NONE
       | dest_monad _ t = case Code_Thingol.split_let t
diff -r d7864276bca8 -r ace701efe203 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Jun 05 07:05:56 2012 +0200
@@ -28,9 +28,10 @@
 
 datatype ml_binding =
     ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
-  | ML_Instance of string * ((class * (string * (vname * sort) list))
-        * ((class * (string * (string * dict list list))) list
-      * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
+  | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
+        superinsts: (class * (string * (string * dict list list))) list,
+        inst_params: ((string * const) * (thm * bool)) list,
+        superinst_params: ((string * const) * (thm * bool)) list };
 
 datatype ml_stmt =
     ML_Exc of string * (typscheme * int)
@@ -83,15 +84,15 @@
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
       (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
-    fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
-          print_app is_pseudo_fun some_thm vars fxy (c, [])
+    fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
+          print_app is_pseudo_fun some_thm vars fxy (const, [])
       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
           str "_"
       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
           str (lookup_var vars v)
       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
-           of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
+           of SOME app => print_app is_pseudo_fun some_thm vars fxy app
             | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
                 print_term is_pseudo_fun some_thm vars BR t2])
       | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
@@ -102,15 +103,15 @@
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map print_abs binds vars;
           in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
-      | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
-          (case Code_Thingol.unfold_const_app t0
-           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
-                then print_case is_pseudo_fun some_thm vars fxy cases
-                else print_app is_pseudo_fun some_thm vars fxy c_ts
-            | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
-    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (arg_tys, _)), _)), ts)) =
+      | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
+          (case Code_Thingol.unfold_const_app (#primitive case_expr)
+           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+                then print_case is_pseudo_fun some_thm vars fxy case_expr
+                else print_app is_pseudo_fun some_thm vars fxy app
+            | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
+    and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
       if is_cons c then
-        let val k = length arg_tys in
+        let val k = length dom in
           if k < 2 orelse length ts = k
           then (str o deresolve) c
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
@@ -118,14 +119,16 @@
         end
       else if is_pseudo_fun c
         then (str o deresolve) c @@ str "()"
-      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
+      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
         @ map (print_term is_pseudo_fun some_thm vars BR) ts
     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
       (print_term is_pseudo_fun) const_syntax some_thm vars
     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
-    and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
+    and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
+          (concat o map str) ["raise", "Fail", "\"empty case\""]
+      | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
           let
-            val (binds, body) = Code_Thingol.unfold_let (ICase cases);
+            val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
             fun print_match ((pat, _), t) vars =
               vars
               |> print_bind is_pseudo_fun some_thm NOBR pat
@@ -139,7 +142,7 @@
               str "end"
             ]
           end
-      | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
+      | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
           let
             fun print_select delim (pat, body) =
               let
@@ -154,9 +157,7 @@
               :: print_select "of" clause
               :: map (print_select "|") clauses
             )
-          end
-      | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
-          (concat o map str) ["raise", "Fail", "\"empty case\""];
+          end;
     fun print_val_decl print_typscheme (name, typscheme) = concat
       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
     fun print_datatype_decl definer (tyco, (vs, cos)) =
@@ -206,7 +207,7 @@
             ))
           end
       | print_def is_pseudo_fun _ definer
-          (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
+          (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
           let
             fun print_super_instance (_, (classrel, x)) =
               concat [
@@ -230,8 +231,8 @@
                   else print_dict_args vs)
               @ str "="
               :: enum "," "{" "}"
-                (map print_super_instance super_instances
-                  @ map print_classparam_instance classparam_instances)
+                (map print_super_instance superinsts
+                  @ map print_classparam_instance inst_params)
               :: str ":"
               @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
             ))
@@ -386,15 +387,15 @@
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
       (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
-    fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
-          print_app is_pseudo_fun some_thm vars fxy (c, [])
+    fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
+          print_app is_pseudo_fun some_thm vars fxy (const, [])
       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
           str "_"
       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
           str (lookup_var vars v)
       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
-           of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
+           of SOME app => print_app is_pseudo_fun some_thm vars fxy app
             | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
                 print_term is_pseudo_fun some_thm vars BR t2])
       | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
@@ -402,15 +403,15 @@
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
             val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
           in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
-      | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
-          (case Code_Thingol.unfold_const_app t0
-           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
-                then print_case is_pseudo_fun some_thm vars fxy cases
-                else print_app is_pseudo_fun some_thm vars fxy c_ts
-            | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
-    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (tys, _)), _)), ts)) =
+      | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
+          (case Code_Thingol.unfold_const_app (#primitive case_expr)
+           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+                then print_case is_pseudo_fun some_thm vars fxy case_expr
+                else print_app is_pseudo_fun some_thm vars fxy app
+            | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
+    and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
       if is_cons c then
-        let val k = length tys in
+        let val k = length dom in
           if length ts = k
           then (str o deresolve) c
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
@@ -418,14 +419,16 @@
         end
       else if is_pseudo_fun c
         then (str o deresolve) c @@ str "()"
-      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
+      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
         @ map (print_term is_pseudo_fun some_thm vars BR) ts
     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
       (print_term is_pseudo_fun) const_syntax some_thm vars
     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
-    and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
+    and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
+          (concat o map str) ["failwith", "\"empty case\""]
+      | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
           let
-            val (binds, body) = Code_Thingol.unfold_let (ICase cases);
+            val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
             fun print_let ((pat, _), t) vars =
               vars
               |> print_bind is_pseudo_fun some_thm NOBR pat
@@ -436,7 +439,7 @@
             brackify_block fxy (Pretty.chunks ps) []
               (print_term is_pseudo_fun some_thm vars' NOBR body)
           end
-      | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
+      | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
           let
             fun print_select delim (pat, body) =
               let
@@ -449,9 +452,7 @@
               :: print_select "with" clause
               :: map (print_select "|") clauses
             )
-          end
-      | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
-          (concat o map str) ["failwith", "\"empty case\""];
+          end;
     fun print_val_decl print_typscheme (name, typscheme) = concat
       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
     fun print_datatype_decl definer (tyco, (vs, cos)) =
@@ -546,7 +547,7 @@
             ))
           end
       | print_def is_pseudo_fun _ definer
-            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
+          (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
           let
             fun print_super_instance (_, (classrel, x)) =
               concat [
@@ -570,8 +571,8 @@
                   else print_dict_args vs)
               @ str "="
               @@ brackets [
-                enum_default "()" ";" "{" "}" (map print_super_instance super_instances
-                  @ map print_classparam_instance classparam_instances),
+                enum_default "()" ";" "{" "}" (map print_super_instance superinsts
+                  @ map print_classparam_instance inst_params),
                 str ":",
                 print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
               ]
@@ -731,7 +732,7 @@
                 | _ => (eqs, NONE)
               else (eqs, NONE)
           in (ML_Function (name, (tysm, eqs')), some_value_name) end
-      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
+      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
           (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
       | ml_binding_of_stmt (name, _) =
           error ("Binding block containing illegal statement: " ^ labelled_name name)
diff -r d7864276bca8 -r ace701efe203 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_printer.ML	Tue Jun 05 07:05:56 2012 +0200
@@ -315,7 +315,7 @@
       |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
 
 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
-    (app as ((c, ((_, (arg_tys, _)), _)), ts)) =
+    (app as ({ name = c, dom, ... }, ts)) =
   case const_syntax c of
     NONE => brackify fxy (print_app_expr some_thm vars app)
   | SOME (Plain_const_syntax (_, s)) =>
@@ -323,7 +323,7 @@
   | SOME (Complex_const_syntax (k, print)) =>
       let
         fun print' fxy ts =
-          print (print_term some_thm) some_thm vars fxy (ts ~~ take k arg_tys);
+          print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
       in
         if k = length ts
         then print' fxy ts
diff -r d7864276bca8 -r ace701efe203 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_scala.ML	Tue Jun 05 07:05:56 2012 +0200
@@ -46,8 +46,8 @@
     fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
     fun print_var vars NONE = str "_"
       | print_var vars (SOME v) = (str o lookup_var vars) v
-    fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
-          print_app tyvars is_pat some_thm vars fxy (c, [])
+    fun print_term tyvars is_pat some_thm vars fxy (IConst const) =
+          print_app tyvars is_pat some_thm vars fxy (const, [])
       | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
           (case Code_Thingol.unfold_const_app t
            of SOME app => print_app tyvars is_pat some_thm vars fxy app
@@ -65,30 +65,30 @@
               print_term tyvars false some_thm vars' NOBR t
             ]
           end
-      | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
-          (case Code_Thingol.unfold_const_app t0
-           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
-                then print_case tyvars some_thm vars fxy cases
-                else print_app tyvars is_pat some_thm vars fxy c_ts
-            | NONE => print_case tyvars some_thm vars fxy cases)
+      | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
+          (case Code_Thingol.unfold_const_app (#primitive case_expr)
+           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+                then print_case tyvars some_thm vars fxy case_expr
+                else print_app tyvars is_pat some_thm vars fxy app
+            | NONE => print_case tyvars some_thm vars fxy case_expr)
     and print_app tyvars is_pat some_thm vars fxy
-        (app as ((c, (((tys, _), (arg_tys, _)), _)), ts)) =
+        (app as ({ name = c, typargs, dom, ... }, ts)) =
       let
         val k = length ts;
-        val tys' = if is_pat orelse
-          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else tys;
+        val typargs' = if is_pat orelse
+          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else typargs;
         val (l, print') = case const_syntax c
          of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
-                  NOBR ((str o deresolve) c) tys') ts)
+                  NOBR ((str o deresolve) c) typargs') ts)
           | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
-                  NOBR (str s) tys') ts)
+                  NOBR (str s) typargs') ts)
           | SOME (Complex_const_syntax (k, print)) =>
               (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
-                (ts ~~ take k arg_tys))
+                (ts ~~ take k dom))
       in if k = l then print' fxy ts
       else if k < l then
         print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
@@ -100,9 +100,11 @@
       end end
     and print_bind tyvars some_thm fxy p =
       gen_print_bind (print_term tyvars true) some_thm fxy p
-    and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
+    and print_case tyvars some_thm vars fxy { clauses = [], ... } =
+          (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"]
+      | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
           let
-            val (bind :: binds, body) = Code_Thingol.unfold_let (ICase cases);
+            val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr);
             fun print_match_val ((pat, ty), t) vars =
               vars
               |> print_bind tyvars some_thm BR pat
@@ -123,7 +125,7 @@
               | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
                   (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
           in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end
-      | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
+      | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
           let
             fun print_select (pat, body) =
               let
@@ -135,9 +137,7 @@
             |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}")
             |> single
             |> enclose "(" ")"
-          end
-      | print_case tyvars some_thm vars fxy ((_, []), _) =
-          (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
+          end;
     fun print_context tyvars vs name = applify "[" "]"
       (fn (v, sort) => (Pretty.block o map str)
         (lookup_tyvar tyvars v :: maps (fn sort => [" : ", deresolve sort]) sort))
@@ -261,19 +261,19 @@
               :: map print_classparam_def classparams
             )
           end
-      | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
-            (super_instances, (classparam_instances, further_classparam_instances)))) =
+      | print_stmt (name, Code_Thingol.Classinst
+          { class, tyco, vs, inst_params, superinst_params, ... }) =
           let
             val tyvars = intro_tyvars vs reserved;
             val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
-            fun print_classparam_instance ((classparam, const as (_, ((_, (tys, _)), _))), (thm, _)) =
+            fun print_classparam_instance ((classparam, const as { dom, ... }), (thm, _)) =
               let
-                val aux_tys = Name.invent_names (snd reserved) "a" tys;
-                val auxs = map fst aux_tys;
+                val aux_dom = Name.invent_names (snd reserved) "a" dom;
+                val auxs = map fst aux_dom;
                 val vars = intro_vars auxs reserved;
                 val aux_abstr = if null auxs then [] else [enum "," "(" ")"
                   (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
-                  (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
+                  (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
               in
                 concat ([str "val", print_method classparam, str "="]
                   @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
@@ -283,7 +283,7 @@
             Pretty.block_enclose (concat [str "implicit def",
               constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
               str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
-                (map print_classparam_instance (classparam_instances @ further_classparam_instances))
+                (map print_classparam_instance (inst_params @ superinst_params))
           end;
   in print_stmt end;
 
diff -r d7864276bca8 -r ace701efe203 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_simp.ML	Tue Jun 05 07:05:56 2012 +0200
@@ -38,8 +38,8 @@
 fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
       ss addsimps (map_filter (fst o snd)) eqs
       |> fold Simplifier.add_cong (the_list some_cong)
-  | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
-      ss addsimps (map (fst o snd) classparam_instances)
+  | add_stmt (Code_Thingol.Classinst { inst_params, ... }) ss =
+      ss addsimps (map (fst o snd) inst_params)
   | add_stmt _ ss = ss;
 
 val add_program = Graph.fold (add_stmt o fst o snd);
diff -r d7864276bca8 -r ace701efe203 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Jun 05 07:05:56 2012 +0200
@@ -18,19 +18,18 @@
       Dict of string list * plain_dict
   and plain_dict = 
       Dict_Const of string * dict list list
-    | Dict_Var of vname * (int * int)
+    | Dict_Var of vname * (int * int);
   datatype itype =
       `%% of string * itype list
     | ITyVar of vname;
-  type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
-    (* (f [T1..Tn] {dicts} (_::S1) .. (_::Sm)) :: S =^= (f, ((([T1..Tn], dicts), ([S1..Sm], S)), ambiguous)) *)
+  type const = { name: string, typargs: itype list, dicts: dict list list,
+    dom: itype list, range: itype, annotate: bool };
   datatype iterm =
       IConst of const
     | IVar of vname option
     | `$ of iterm * iterm
     | `|=> of (vname option * itype) * iterm
-    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
-        (*((term, type), [(selector pattern, body term )]), primitive term)*)
+    | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
   val `$$ : iterm * iterm list -> iterm;
   val `|==> : (vname option * itype) list * iterm -> iterm;
   type typscheme = (vname * sort) list * itype;
@@ -77,10 +76,10 @@
     | Class of class * (vname * ((class * string) list * (string * itype) list))
     | Classrel of class * class
     | Classparam of string * class
-    | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
-          * ((class * (string * (string * dict list list))) list (*super instances*)
-        * (((string * const) * (thm * bool)) list (*class parameter instances*)
-          * ((string * const) * (thm * bool)) list (*super class parameter instances*)))
+    | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
+        superinsts: (class * (string * (string * dict list list))) list,
+        inst_params: ((string * const) * (thm * bool)) list,
+        superinst_params: ((string * const) * (thm * bool)) list };
   type program = stmt Graph.T
   val empty_funs: program -> string list
   val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
@@ -126,7 +125,7 @@
   case dest x
    of NONE => ([], x)
     | SOME (x1, x2) =>
-        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
+        let val (xs', x') = unfoldr dest x2 in (x1 :: xs', x') end;
 
 
 (** language core - types, terms **)
@@ -137,21 +136,21 @@
     Dict of string list * plain_dict
 and plain_dict = 
     Dict_Const of string * dict list list
-  | Dict_Var of vname * (int * int)
+  | Dict_Var of vname * (int * int);
 
 datatype itype =
     `%% of string * itype list
   | ITyVar of vname;
 
-type const = string * (((itype list * dict list list) *
-  (itype list (*types of arguments*) * itype (*result type*))) * bool (*requires type annotation*))
+type const = { name: string, typargs: itype list, dicts: dict list list,
+  dom: itype list, range: itype, annotate: bool };
 
 datatype iterm =
     IConst of const
   | IVar of vname option
   | `$ of iterm * iterm
   | `|=> of (vname option * itype) * iterm
-  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
+  | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
     (*see also signature*)
 
 fun is_IVar (IVar _) = true
@@ -172,7 +171,7 @@
     | _ => NONE);
 
 val split_let = 
-  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
+  (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body)
     | _ => NONE);
 
 val unfold_let = unfoldr split_let;
@@ -188,16 +187,16 @@
       | fold' (IVar _) = I
       | fold' (t1 `$ t2) = fold' t1 #> fold' t2
       | fold' (_ `|=> t) = fold' t
-      | fold' (ICase (((t, _), ds), _)) = fold' t
-          #> fold (fn (pat, body) => fold' pat #> fold' body) ds
+      | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t
+          #> fold (fn (p, body) => fold' p #> fold' body) clauses
   in fold' end;
 
-val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c);
+val add_constnames = fold_constexprs (fn { name = c, ... } => insert (op =) c);
 
 fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
   | add_tycos (ITyVar _) = I;
 
-val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
+val add_tyconames = fold_constexprs (fn { typargs = tys, ... } => fold add_tycos tys);
 
 fun fold_varnames f =
   let
@@ -209,7 +208,7 @@
           | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
           | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
           | fold_term vs ((NONE, _) `|=> t) = fold_term vs t
-          | fold_term vs (ICase (((t, _), ds), _)) = fold_term vs t #> fold (fold_case vs) ds
+          | fold_term vs (ICase { term = t, clauses = clauses, ... }) = fold_term vs t #> fold (fold_case vs) clauses
         and fold_case vs (p, t) = fold_term (add p vs) t;
       in fold_term [] end;
     fun add t = fold_aux add (insert (op =)) t;
@@ -219,9 +218,9 @@
 
 fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
   | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
-     of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
-          if v = w andalso (exists_var p v orelse not (exists_var t' v))
-          then ((p, ty), t')
+     of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } =>
+          if v = w andalso (exists_var p v orelse not (exists_var body v))
+          then ((p, ty), body)
           else ((IVar (SOME v), ty), t)
       | _ => ((IVar (SOME v), ty), t))
   | split_pat_abs _ = NONE;
@@ -239,27 +238,27 @@
         val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
       in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
 
-fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) =
+fun eta_expand k (const as { name = c, dom = tys, ... }, ts) =
   let
     val j = length ts;
     val l = k - j;
     val _ = if l > length tys
-      then error ("Impossible eta-expansion for constant " ^ quote name) else ();
+      then error ("Impossible eta-expansion for constant " ^ quote c) else ();
     val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
     val vs_tys = (map o apfst) SOME
       (Name.invent_names ctxt "a" ((take l o drop j) tys));
-  in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
+  in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
 
 fun contains_dict_var t =
   let
     fun cont_dict (Dict (_, d)) = cont_plain_dict d
     and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
       | cont_plain_dict (Dict_Var _) = true;
-    fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
+    fun cont_term (IConst { dicts = dss, ... }) = (exists o exists) cont_dict dss
       | cont_term (IVar _) = false
       | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
       | cont_term (_ `|=> t) = cont_term t
-      | cont_term (ICase (_, t)) = cont_term t;
+      | cont_term (ICase { primitive = t, ... }) = cont_term t;
   in cont_term t end;
 
 
@@ -427,11 +426,10 @@
   | Class of class * (vname * ((class * string) list * (string * itype) list))
   | Classrel of class * class
   | Classparam of string * class
-  | Classinst of (class * (string * (vname * sort) list))
-        * ((class * (string * (string * dict list list))) list
-      * (((string * const) * (thm * bool)) list
-        * ((string * const) * (thm * bool)) list))
-      (*see also signature*);
+  | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
+      superinsts: (class * (string * (string * dict list list))) list,
+      inst_params: ((string * const) * (thm * bool)) list,
+      superinst_params: ((string * const) * (thm * bool)) list };
 
 type program = stmt Graph.T;
 
@@ -444,9 +442,10 @@
       (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
   | map_terms_bottom_up f ((v, ty) `|=> t) = f
       ((v, ty) `|=> map_terms_bottom_up f t)
-  | map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f
-      (ICase (((map_terms_bottom_up f t, ty), (map o pairself)
-        (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
+  | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
+      (ICase { term = map_terms_bottom_up f t, typ = ty,
+        clauses = (map o pairself) (map_terms_bottom_up f) clauses,
+        primitive = map_terms_bottom_up f t0 });
 
 fun map_classparam_instances_as_term f =
   (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
@@ -459,8 +458,11 @@
   | map_terms_stmt f (stmt as Class _) = stmt
   | map_terms_stmt f (stmt as Classrel _) = stmt
   | map_terms_stmt f (stmt as Classparam _) = stmt
-  | map_terms_stmt f (Classinst (arity, (super_instances, classparam_instances))) =
-      Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances));
+  | map_terms_stmt f (Classinst { class, tyco, vs, superinsts,
+      inst_params, superinst_params }) =
+        Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts,
+          inst_params = map_classparam_instances_as_term f inst_params,
+          superinst_params = map_classparam_instances_as_term f superinst_params };
 
 fun is_cons program name = case Graph.get_node program name
  of Datatypecons _ => true
@@ -484,7 +486,7 @@
           quote (Proof_Context.extern_class ctxt sub ^ " < " ^ Proof_Context.extern_class ctxt super)
         end
     | Classparam (c, _) => quote (Code.string_of_const thy c)
-    | Classinst ((class, (tyco, _)), _) =>
+    | Classinst { class, tyco, ... } =>
         let
           val Class (class, _) = Graph.get_node program class;
           val Datatype (tyco, _) = Graph.get_node program tyco;
@@ -678,9 +680,9 @@
 and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
   let
     val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
-    val these_classparams = these o try (#params o AxClass.get_info thy);
-    val classparams = these_classparams class;
-    val further_classparams = maps these_classparams
+    val these_class_params = these o try (#params o AxClass.get_info thy);
+    val class_params = these_class_params class;
+    val superclass_params = maps these_class_params
       ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
     val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
     val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
@@ -710,12 +712,11 @@
       ##>> ensure_tyco thy algbr eqngr permissive tyco
       ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
       ##>> fold_map translate_super_instance super_classes
-      ##>> fold_map translate_classparam_instance classparams
-      ##>> fold_map translate_classparam_instance further_classparams
-      #>> (fn (((((class, tyco), arity_args), super_instances),
-        classparam_instances), further_classparam_instances) =>
-          Classinst ((class, (tyco, arity_args)), (super_instances,
-            (classparam_instances, further_classparam_instances))));
+      ##>> fold_map translate_classparam_instance class_params
+      ##>> fold_map translate_classparam_instance superclass_params
+      #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
+          Classinst { class = class, tyco = tyco, vs = vs,
+            superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
   in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
 and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
       pair (ITyVar (unprefix "'" v))
@@ -759,17 +760,18 @@
         then translation_error thy permissive some_thm
           "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
       else ()
-    val (annotate, ty') = dest_tagged_type ty
-    val arg_typs = Sign.const_typargs thy (c, ty');
+    val (annotate, ty') = dest_tagged_type ty;
+    val typargs = Sign.const_typargs thy (c, ty');
     val sorts = Code_Preproc.sortargs eqngr c;
-    val (function_typs, body_typ) = Term.strip_type ty';
+    val (dom, range) = Term.strip_type ty';
   in
     ensure_const thy algbr eqngr permissive c
-    ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
-    ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
-    ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
-    #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
-      IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
+    ##>> fold_map (translate_typ thy algbr eqngr permissive) typargs
+    ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
+    ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
+    #>> (fn (((c, typargs), dss), range :: dom) =>
+      IConst { name = c, typargs = typargs, dicts = dss,
+        dom = dom, range = range, annotate = annotate })
   end
 and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
   translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
@@ -788,22 +790,22 @@
     val constrs =
       if null case_pats then []
       else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
-    fun casify naming constrs ty ts =
+    fun casify naming constrs ty t_app ts =
       let
         val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
         fun collapse_clause vs_map ts body =
           let
           in case body
-           of IConst (c, _) => if member (op =) undefineds c
+           of IConst { name = c, ... } => if member (op =) undefineds c
                 then []
                 else [(ts, body)]
-            | ICase (((IVar (SOME v), _), subclauses), _) =>
+            | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
                 if forall (fn (pat', body') => exists_var pat' v
-                  orelse not (exists_var body' v)) subclauses
+                  orelse not (exists_var body' v)) clauses
                 then case AList.lookup (op =) vs_map v
                  of SOME i => maps (fn (pat', body') =>
                       collapse_clause (AList.delete (op =) v vs_map)
-                        (nth_map i (K pat') ts) body') subclauses
+                        (nth_map i (K pat') ts) body') clauses
                   | NONE => [(ts, body)]
                 else [(ts, body)]
             | _ => [(ts, body)]
@@ -818,11 +820,11 @@
         val ts_clause = nth_drop t_pos ts;
         val clauses = if null case_pats
           then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
-          else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
+          else maps (fn ((constr as IConst { dom = tys, ... }, n), t) =>
             mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
               (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t)
                 (case_pats ~~ ts_clause)));
-      in ((t, ty), clauses) end;
+      in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end;
   in
     translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
     ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
@@ -830,7 +832,7 @@
     ##>> translate_typ thy algbr eqngr permissive ty
     ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
     #-> (fn (((t, constrs), ty), ts) =>
-      `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
+      `(fn (_, (naming, _)) => casify naming constrs ty t ts))
   end
 and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   if length ts < num_args then
diff -r d7864276bca8 -r ace701efe203 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/Tools/nbe.ML	Tue Jun 05 07:05:56 2012 +0200
@@ -314,13 +314,13 @@
           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 { name = c, dicts = dss, ... }) ts = constapp c dss ts
           | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
           | of_iapp match_cont ((v, _) `|=> t) ts =
               nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
-          | of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
+          | of_iapp match_cont (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts =
               nbe_apps (ml_cases (of_iterm NONE t)
-                (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs
+                (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) clauses
                   @ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts
       in of_iterm end;
 
@@ -345,7 +345,7 @@
               |> subst_vars t1
               ||>> subst_vars t2
               |>> (op `$)
-          | subst_vars (ICase (_, t)) samepairs = subst_vars t samepairs;
+          | subst_vars (ICase { primitive = t, ... }) samepairs = subst_vars t samepairs;
         val (args', _) = fold_map subst_vars args samepairs;
       in (samepairs, args') end;
 
@@ -410,6 +410,10 @@
 
 (* extract equations from statements *)
 
+fun dummy_const c dss =
+  IConst { name = c, typargs = [], dicts = dss,
+    dom = [], range = ITyVar "", annotate = false };
+
 fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
       []
   | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
@@ -424,17 +428,17 @@
         val params = Name.invent Name.context "d" (length names);
         fun mk (k, name) =
           (name, ([(v, [])],
-            [([IConst (class, ((([], []), ([], ITyVar "")), false)) `$$ map (IVar o SOME) params],
+            [([dummy_const class [] `$$ map (IVar o SOME) params],
               IVar (SOME (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, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
-      [(inst, (arity_args, [([], IConst (class, ((([], []), ([], ITyVar "")), false)) `$$
-        map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), ([], ITyVar "")), false))) super_instances
-        @ map (IConst o snd o fst) classparam_instances)]))];
+  | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) =
+      [(inst, (vs, [([], dummy_const class [] `$$
+        map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts
+        @ map (IConst o snd o fst) inst_params)]))];
 
 
 (* compile whole programs *)