src/Tools/Code/code_thingol.ML
changeset 37445 e372fa3c7239
parent 37440 a5d44161ba2a
child 37446 fc55011cfdfd
     1.1 --- a/src/Tools/Code/code_thingol.ML	Thu Jun 17 10:45:10 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jun 17 10:51:38 2010 +0200
     1.3 @@ -73,8 +73,7 @@
     1.4      | Classrel of class * class
     1.5      | Classparam of string * class
     1.6      | Classinst of (class * (string * (vname * sort) list) (*class and arity*) )
     1.7 -          * (((class * (string * (string * dict list list))) list (*super instances*)
     1.8 -            * (class * class) list list (*type argument weakening mapping*))
     1.9 +          * ((class * (string * (string * dict list list))) list (*super instances*)
    1.10          * ((string * const) * (thm * bool)) list (*class parameter instances*))
    1.11    type program = stmt Graph.T
    1.12    val empty_funs: program -> string list
    1.13 @@ -410,8 +409,7 @@
    1.14    | Classrel of class * class
    1.15    | Classparam of string * class
    1.16    | Classinst of (class * (string * (vname * sort) list))
    1.17 -        * (((class * (string * (string * dict list list))) list
    1.18 -          * (class * class) list list)
    1.19 +        * ((class * (string * (string * dict list list))) list
    1.20        * ((string * const) * (thm * bool)) list) (*see also signature*);
    1.21  
    1.22  type program = stmt Graph.T;
    1.23 @@ -438,8 +436,8 @@
    1.24    | map_terms_stmt f (stmt as Class _) = stmt
    1.25    | map_terms_stmt f (stmt as Classrel _) = stmt
    1.26    | map_terms_stmt f (stmt as Classparam _) = stmt
    1.27 -  | map_terms_stmt f (Classinst (arity, ((super_instances, weakening), classparams))) =
    1.28 -      Classinst (arity, ((super_instances, weakening), (map o apfst o apsnd) (fn const =>
    1.29 +  | map_terms_stmt f (Classinst (arity, (super_instances, classparams))) =
    1.30 +      Classinst (arity, (super_instances, (map o apfst o apsnd) (fn const =>
    1.31          case f (IConst const) of IConst const' => const') classparams));
    1.32  
    1.33  fun is_cons program name = case Graph.get_node program name
    1.34 @@ -640,7 +638,7 @@
    1.35        ##>> fold_map translate_super_instance super_classes
    1.36        ##>> fold_map translate_classparam_instance classparams
    1.37        #>> (fn ((((class, tyco), arity_args), super_instances), classparam_instances) =>
    1.38 -             Classinst ((class, (tyco, arity_args)), ((super_instances, []), classparam_instances)));
    1.39 +             Classinst ((class, (tyco, arity_args)), (super_instances, classparam_instances)));
    1.40    in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
    1.41  and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
    1.42        pair (ITyVar (unprefix "'" v))