diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -21,7 +21,7 @@
 structure Fun_Pred = Theory_Data
 (
   type T = (term * term) Item_Net.T;
-  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
+  val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst);
   val extend = I;
   val merge = Item_Net.merge;
 )
@@ -295,7 +295,7 @@
           map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
         dst_prednames
       val thy'' = Fun_Pred.map
-        (fold Item_Net.update (map (pairself Logic.varify_global)
+        (fold Item_Net.update (map (apply2 Logic.varify_global)
           (dst_funs ~~ dst_preds))) thy'
       fun functional_mode_of T =
         list_fun_mode (replicate (length (binder_types T)) Input @ [Output])