src/HOL/Tools/old_primrec.ML

--- a/src/HOL/Tools/old_primrec.ML	Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Wed May 05 18:25:34 2010 +0200
@@ -120,7 +120,7 @@
           let
             val (f, ts) = strip_comb t;
           in
-            if is_Const f andalso dest_Const f mem map fst rec_eqns then
+            if is_Const f andalso member (op =) (map fst rec_eqns) (dest_Const f) then
               let
                 val fnameT' as (fname', _) = dest_Const f;
                 val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');