src/Tools/Code/code_ml.ML
changeset 37449 034ebe92f090
parent 37447 ad3e04f289b6
child 37745 6315b6426200
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Jun 17 15:59:46 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jun 17 15:59:47 2010 +0200
     1.3 @@ -33,13 +33,13 @@
     1.4      ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     1.5    | ML_Instance of string * ((class * (string * (vname * sort) list))
     1.6          * ((class * (string * (string * dict list list))) list
     1.7 -      * ((string * const) * (thm * bool)) list));
     1.8 +      * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
     1.9  
    1.10  datatype ml_stmt =
    1.11      ML_Exc of string * (typscheme * int)
    1.12    | ML_Val of ml_binding
    1.13    | ML_Funs of ml_binding list * string list
    1.14 -  | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
    1.15 +  | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
    1.16    | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
    1.17  
    1.18  fun stmt_name_of_binding (ML_Function (name, _)) = name
    1.19 @@ -121,9 +121,9 @@
    1.20                  then print_case is_pseudo_fun some_thm vars fxy cases
    1.21                  else print_app is_pseudo_fun some_thm vars fxy c_ts
    1.22              | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
    1.23 -    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
    1.24 +    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =
    1.25        if is_cons c then
    1.26 -        let val k = length tys in
    1.27 +        let val k = length function_typs in
    1.28            if k < 2 orelse length ts = k
    1.29            then (str o deresolve) c
    1.30              :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
    1.31 @@ -174,8 +174,8 @@
    1.32        [str "val", str (deresolve name), str ":", print_typscheme typscheme];
    1.33      fun print_datatype_decl definer (tyco, (vs, cos)) =
    1.34        let
    1.35 -        fun print_co (co, []) = str (deresolve co)
    1.36 -          | print_co (co, tys) = concat [str (deresolve co), str "of",
    1.37 +        fun print_co ((co, _), []) = str (deresolve co)
    1.38 +          | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
    1.39                enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
    1.40        in
    1.41          concat (
    1.42 @@ -219,7 +219,7 @@
    1.43              ))
    1.44            end
    1.45        | print_def is_pseudo_fun _ definer
    1.46 -          (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
    1.47 +          (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
    1.48            let
    1.49              fun print_super_instance (_, (classrel, dss)) =
    1.50                concat [
    1.51 @@ -466,8 +466,8 @@
    1.52        [str "val", str (deresolve name), str ":", print_typscheme typscheme];
    1.53      fun print_datatype_decl definer (tyco, (vs, cos)) =
    1.54        let
    1.55 -        fun print_co (co, []) = str (deresolve co)
    1.56 -          | print_co (co, tys) = concat [str (deresolve co), str "of",
    1.57 +        fun print_co ((co, _), []) = str (deresolve co)
    1.58 +          | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
    1.59                enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
    1.60        in
    1.61          concat (
    1.62 @@ -554,7 +554,7 @@
    1.63              ))
    1.64            end
    1.65        | print_def is_pseudo_fun _ definer
    1.66 -            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
    1.67 +            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
    1.68            let
    1.69              fun print_super_instance (_, (classrel, dss)) =
    1.70                concat [