diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -274,7 +274,7 @@
         | [] => fixrec_err "no defining equations for function"
         | _ => fixrec_err "all equations in block must define the same function"
     val vars =
-        case distinct (op = o pairself length) (map fst matchers) of
+        case distinct (op = o apply2 length) (map fst matchers) of
           [vars] => vars
         | _ => fixrec_err "all equations in block must have the same arity"
     (* rename so all matchers use same free variables *)