--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Nov 26 20:05:34 2014 +0100
@@ -390,7 +390,7 @@
(if Ts1 = Ts2 andalso length Ts1 = 1 then "itself" else qsotys Ts2));
val sorted_actual_Ts =
- sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts;
+ sort (prod_ord int_ord Term_Ord.typ_ord o apply2 (`Term.size_of_typ)) actual_Ts;
fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s)));