# HG changeset patch
# User haftmann
# Date 1276764698 -7200
# Node ID e372fa3c7239affbd09d6eab8fd58bca5aed3743
# Parent  2e7e7ff21e25f26e4b1cec5223b1a1ecf01aa262
dropped obscure type argument weakening mapping -- was only a misunderstanding

diff -r 2e7e7ff21e25 -r e372fa3c7239 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Jun 17 10:45:10 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Jun 17 10:51:38 2010 +0200
@@ -32,7 +32,7 @@
 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 * (class * class) list list)
+        * ((class * (string * (string * dict list list))) list
       * ((string * const) * (thm * bool)) list));
 
 datatype ml_stmt =
@@ -219,7 +219,7 @@
             ))
           end
       | print_def is_pseudo_fun _ definer
-          (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
+          (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
           let
             fun print_super_instance (_, (classrel, dss)) =
               concat [
@@ -554,7 +554,7 @@
             ))
           end
       | print_def is_pseudo_fun _ definer
-            (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
+            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
           let
             fun print_super_instance (_, (classrel, dss)) =
               concat [
diff -r 2e7e7ff21e25 -r e372fa3c7239 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Jun 17 10:45:10 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Jun 17 10:51:38 2010 +0200
@@ -252,7 +252,7 @@
             )
           end
       | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
-            ((super_instances, _), classparam_instances))) =
+            (super_instances, classparam_instances))) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
             val insttyp = tyco `%% map (ITyVar o fst) vs;
diff -r 2e7e7ff21e25 -r e372fa3c7239 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Jun 17 10:45:10 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Jun 17 10:51:38 2010 +0200
@@ -73,8 +73,7 @@
     | 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*)
-            * (class * class) list list (*type argument weakening mapping*))
+          * ((class * (string * (string * dict list list))) list (*super instances*)
         * ((string * const) * (thm * bool)) list (*class parameter instances*))
   type program = stmt Graph.T
   val empty_funs: program -> string list
@@ -410,8 +409,7 @@
   | Classrel of class * class
   | Classparam of string * class
   | Classinst of (class * (string * (vname * sort) list))
-        * (((class * (string * (string * dict list list))) list
-          * (class * class) list list)
+        * ((class * (string * (string * dict list list))) list
       * ((string * const) * (thm * bool)) list) (*see also signature*);
 
 type program = stmt Graph.T;
@@ -438,8 +436,8 @@
   | 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, weakening), classparams))) =
-      Classinst (arity, ((super_instances, weakening), (map o apfst o apsnd) (fn const =>
+  | map_terms_stmt f (Classinst (arity, (super_instances, classparams))) =
+      Classinst (arity, (super_instances, (map o apfst o apsnd) (fn const =>
         case f (IConst const) of IConst const' => const') classparams));
 
 fun is_cons program name = case Graph.get_node program name
@@ -640,7 +638,7 @@
       ##>> fold_map translate_super_instance super_classes
       ##>> fold_map translate_classparam_instance classparams
       #>> (fn ((((class, tyco), arity_args), super_instances), classparam_instances) =>
-             Classinst ((class, (tyco, arity_args)), ((super_instances, []), classparam_instances)));
+             Classinst ((class, (tyco, arity_args)), (super_instances, classparam_instances)));
   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))
diff -r 2e7e7ff21e25 -r e372fa3c7239 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu Jun 17 10:45:10 2010 +0200
+++ b/src/Tools/nbe.ML	Thu Jun 17 10:51:38 2010 +0200
@@ -417,7 +417,7 @@
       []
   | eqns_of_stmt (_, Code_Thingol.Classparam _) =
       []
-  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), ((super_instances, _), classparam_instances))) =
+  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, classparam_instances))) =
       [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
         map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
         @ map (IConst o snd o fst) classparam_instances)]))];