src/HOL/HOLCF/Tools/fixrec.ML
changeset 59058 a78612c67ec0
parent 58957 c9e744ea8a38
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -274,7 +274,7 @@
     1.4          | [] => fixrec_err "no defining equations for function"
     1.5          | _ => fixrec_err "all equations in block must define the same function"
     1.6      val vars =
     1.7 -        case distinct (op = o pairself length) (map fst matchers) of
     1.8 +        case distinct (op = o apply2 length) (map fst matchers) of
     1.9            [vars] => vars
    1.10          | _ => fixrec_err "all equations in block must have the same arity"
    1.11      (* rename so all matchers use same free variables *)