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