src/HOL/Tools/SMT/smt_datatypes.ML
changeset 58460 a88eb33058f7
parent 58430 73df5884edcf
child 58634 9f10d82e8188
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Fri Sep 26 14:41:15 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Fri Sep 26 14:41:54 2014 +0200
     1.3 @@ -71,13 +71,13 @@
     1.4        | info :: _ => (map (pair (hd fps)) (get_typedef_decl info T Ts), ctxt))
     1.5    in
     1.6      (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
     1.7 -      SOME {fp, fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} =>
     1.8 +      SOME {fp, fp_res = {Ts = fp_Ts, ...}, fp_ctr_sugar = {ctr_sugar, ...}, ...} =>
     1.9        if member (op =) fps fp then
    1.10          let
    1.11            val ns = map (fst o dest_Type) fp_Ts
    1.12            val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns
    1.13            val Xs = map #X mutual_fp_sugars
    1.14 -          val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars
    1.15 +          val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) mutual_fp_sugars
    1.16  
    1.17            (* Datatypes nested through datatypes and codatatypes nested through codatatypes are
    1.18               allowed. So are mutually (co)recursive (co)datatypes. *)