src/Tools/Code/code_ml.ML
changeset 41118 b290841cd3b0
parent 41100 6c0940392fb4
child 41343 71f4f15258a5
     1.1 --- a/src/Tools/Code/code_ml.ML	Mon Dec 13 10:15:27 2010 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Mon Dec 13 22:54:47 2010 +0100
     1.3 @@ -80,16 +80,18 @@
     1.4        | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]
     1.5        | print_classrels fxy classrels ps =
     1.6            brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]
     1.7 -    fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
     1.8 -          print_classrels fxy classrels ((str o deresolve) inst ::
     1.9 +    fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
    1.10 +      print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
    1.11 +    and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
    1.12 +          ((str o deresolve) inst ::
    1.13              (if is_pseudo_fun inst then [str "()"]
    1.14              else map_filter (print_dicts is_pseudo_fun BR) dss))
    1.15 -      | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
    1.16 -          print_classrels fxy classrels [str (if k = 1 then first_upper v ^ "_"
    1.17 +      | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
    1.18 +          [str (if k = 1 then first_upper v ^ "_"
    1.19              else first_upper v ^ string_of_int (i+1) ^ "_")]
    1.20      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    1.21      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    1.22 -      (map_index (fn (i, _) => Dict_Var ([], (v, (i, length sort)))) sort));
    1.23 +      (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
    1.24      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    1.25            print_app is_pseudo_fun some_thm vars fxy (c, [])
    1.26        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    1.27 @@ -219,7 +221,7 @@
    1.28                concat [
    1.29                  (str o Long_Name.base_name o deresolve) classrel,
    1.30                  str "=",
    1.31 -                print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
    1.32 +                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
    1.33                ];
    1.34              fun print_classparam_instance ((classparam, const), (thm, _)) =
    1.35                concat [
    1.36 @@ -380,18 +382,19 @@
    1.37      fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
    1.38      val print_classrels =
    1.39        fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])
    1.40 -    fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
    1.41 +    fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
    1.42 +      print_plain_dict is_pseudo_fun fxy x
    1.43 +      |> print_classrels classrels
    1.44 +    and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
    1.45            brackify BR ((str o deresolve) inst ::
    1.46              (if is_pseudo_fun inst then [str "()"]
    1.47              else map_filter (print_dicts is_pseudo_fun BR) dss))
    1.48 -          |> print_classrels classrels
    1.49 -      | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
    1.50 +      | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
    1.51            str (if k = 1 then "_" ^ first_upper v
    1.52              else "_" ^ first_upper v ^ string_of_int (i+1))
    1.53 -          |> print_classrels classrels
    1.54      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    1.55      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    1.56 -      (map_index (fn (i, _) => Dict_Var ([], (v, (i, length sort)))) sort));
    1.57 +      (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
    1.58      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    1.59            print_app is_pseudo_fun some_thm vars fxy (c, [])
    1.60        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    1.61 @@ -556,7 +559,7 @@
    1.62                concat [
    1.63                  (str o deresolve) classrel,
    1.64                  str "=",
    1.65 -                print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
    1.66 +                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
    1.67                ];
    1.68              fun print_classparam_instance ((classparam, const), (thm, _)) =
    1.69                concat [