src/HOL/Tools/SMT/smt_datatypes.ML
changeset 58634 9f10d82e8188
parent 58460 a88eb33058f7
child 59020 a86683d6c97e
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Oct 08 14:34:30 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Oct 08 17:09:07 2014 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  
     1.5      val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0
     1.6    in
     1.7 -    Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
     1.8 +    @{fold_map 2} mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
     1.9      |>> (pair T #> single)
    1.10    end
    1.11