src/ZF/Tools/primrec_package.ML
changeset 33037 b22e44496dc2
parent 30364 577edc39b501
child 33038 8f9594c31de4
     1.1 --- a/src/ZF/Tools/primrec_package.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4    in
     1.5      if has_duplicates (op =) lfrees then
     1.6        raise RecError "repeated variable name in pattern"
     1.7 -    else if not ((map dest_Free (OldTerm.term_frees rhs)) subset lfrees) then
     1.8 +    else if not (gen_subset (op =) (Term.add_frees rhs [], lfrees)) then
     1.9        raise RecError "extra variables on rhs"
    1.10      else if length middle > 1 then
    1.11        raise RecError "more than one non-variable in pattern"