--- a/src/ZF/Tools/primrec_package.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/ZF/Tools/primrec_package.ML Tue Oct 20 16:13:01 2009 +0200
@@ -65,7 +65,7 @@
in
if has_duplicates (op =) lfrees then
raise RecError "repeated variable name in pattern"
- else if not ((map dest_Free (OldTerm.term_frees rhs)) subset lfrees) then
+ else if not (gen_subset (op =) (Term.add_frees rhs [], lfrees)) then
raise RecError "extra variables on rhs"
else if length middle > 1 then
raise RecError "more than one non-variable in pattern"