src/HOL/Tools/SMT/smt_datatypes.ML
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