--- a/src/HOL/Tools/old_primrec.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML Wed Oct 21 10:15:31 2009 +0200
@@ -90,7 +90,7 @@
else
(check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
check_vars "extra variables on rhs: "
- (map dest_Free (OldTerm.term_frees rhs) \\ lfrees);
+ (subtract (op =) lfrees (map dest_Free (OldTerm.term_frees rhs)));
case AList.lookup (op =) rec_fns fnameT of
NONE =>
(fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns