transitive superclasses were also only a misunderstanding

--- a/src/Tools/Code/code_haskell.ML	Thu Jun 17 10:57:00 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Jun 17 11:33:04 2010 +0200
@@ -194,7 +194,7 @@
               @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
             )
           end
-      | print_stmt (name, Code_Thingol.Class (_, (v, ((super_classes, _), classparams)))) =
+      | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
           let
             val tyvars = intro_vars [v] reserved;
             fun print_classparam (classparam, ty) =

--- a/src/Tools/Code/code_ml.ML	Thu Jun 17 10:57:00 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Jun 17 11:33:04 2010 +0200
@@ -40,7 +40,7 @@
   | ML_Val of ml_binding
   | ML_Funs of ml_binding list * string list
   | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
-  | ML_Class of string * (vname * (((class * string) list * (class * string) list) * (string * itype) list));
+  | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
 
 fun stmt_name_of_binding (ML_Function (name, _)) = name
   | stmt_name_of_binding (ML_Instance (name, _)) = name;
@@ -301,7 +301,7 @@
             sig_ps
             (Pretty.chunks (ps @| semicolon [p]))
           end
-     | print_stmt (ML_Class (class, (v, ((super_classes, _), classparams)))) =
+     | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
           let
             fun print_field s p = concat [str s, str ":", p];
             fun print_proj s p = semicolon
@@ -635,7 +635,7 @@
             sig_ps
             (Pretty.chunks (ps @| doublesemicolon [p]))
           end
-     | print_stmt (ML_Class (class, (v, ((super_classes, _), classparams)))) =
+     | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
           let
             fun print_field s p = concat [str s, str ":", p];
             fun print_super_class_field (super_class, classrel) =

--- a/src/Tools/Code/code_scala.ML	Thu Jun 17 10:57:00 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Jun 17 11:33:04 2010 +0200
@@ -212,7 +212,7 @@
               :: map print_co cos
             )
           end
-      | print_stmt (name, Code_Thingol.Class (_, (v, ((super_classes, all_super_classes), classparams)))) =
+      | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
           let
             val tyvars = intro_vars [v] reserved;
             val vs = [(v, [name])];

--- a/src/Tools/Code/code_thingol.ML	Thu Jun 17 10:57:00 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Jun 17 11:33:04 2010 +0200
@@ -69,13 +69,10 @@
     | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
     | Datatype of string * ((vname * sort) list * (string * itype list) list)
     | Datatypecons of string * string
-    | Class of class * (vname
-        * (((class * string) list (*direct superclasses*)
-          * (class * string) list) (*indirect superclasses*)
-            * (string * itype) list (*class operations*)))
+    | 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*))
+    | 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*))
   type program = stmt Graph.T
@@ -403,17 +400,17 @@
 (** statements, abstract programs **)
 
 type typscheme = (vname * sort) list * itype;
-datatype stmt = (*see also signature*)
+datatype stmt =
     NoStmt
   | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
   | Datatype of string * ((vname * sort) list * (string * itype list) list)
   | Datatypecons of string * string
-  | Class of class * (vname * (((class * string) list * (class * string) list) * (string * itype) list))
+  | 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*);
 
 type program = stmt Graph.T;
 
@@ -596,7 +593,6 @@
     val stmt_class =
       fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
         ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
-      ##>> pair [] (*FIXME*)
       ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
         ##>> translate_typ thy algbr eqngr permissive ty) cs
       #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))

--- a/src/Tools/nbe.ML	Thu Jun 17 10:57:00 2010 +0200
+++ b/src/Tools/nbe.ML	Thu Jun 17 11:33:04 2010 +0200
@@ -404,7 +404,7 @@
       []
   | eqns_of_stmt (_, Code_Thingol.Datatype _) =
       []
-  | eqns_of_stmt (class, Code_Thingol.Class (_, (v, ((super_classes, _), classparams)))) =
+  | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
       let
         val names = map snd super_classes @ map fst classparams;
         val params = Name.invent_list [] "d" (length names);