src/Tools/Code/code_ml.ML
changeset 52519 598addf65209
parent 52435 6646bb548c6b
child 55145 2bb3cd36bcf7
     1.1 --- a/src/Tools/Code/code_ml.ML	Wed Jul 03 23:42:07 2013 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jul 04 08:52:44 2013 +0200
     1.3 @@ -30,8 +30,8 @@
     1.4      ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     1.5    | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
     1.6          superinsts: (class * (string * (string * dict list list))) list,
     1.7 -        inst_params: ((string * const) * (thm * bool)) list,
     1.8 -        superinst_params: ((string * const) * (thm * bool)) list };
     1.9 +        inst_params: ((string * (const * int)) * (thm * bool)) list,
    1.10 +        superinst_params: ((string * (const * int)) * (thm * bool)) list };
    1.11  
    1.12  datatype ml_stmt =
    1.13      ML_Exc of string * (typscheme * int)
    1.14 @@ -215,7 +215,7 @@
    1.15                  str "=",
    1.16                  print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
    1.17                ];
    1.18 -            fun print_classparam_instance ((classparam, const), (thm, _)) =
    1.19 +            fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
    1.20                concat [
    1.21                  (str o Long_Name.base_name o deresolve) classparam,
    1.22                  str "=",
    1.23 @@ -552,7 +552,7 @@
    1.24                  str "=",
    1.25                  print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
    1.26                ];
    1.27 -            fun print_classparam_instance ((classparam, const), (thm, _)) =
    1.28 +            fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
    1.29                concat [
    1.30                  (str o deresolve) classparam,
    1.31                  str "=",