--- a/src/HOL/Nominal/nominal_primrec.ML Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Nominal/nominal_primrec.ML
- Author: Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
+ Author: Norbert Voelker, FernUni Hagen
+ Author: Stefan Berghofer, TU Muenchen
Package for defining functions on nominal datatypes by primitive recursion.
Taken from HOL/Tools/primrec_package.ML
@@ -71,7 +72,7 @@
else
(check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
check_vars "extra variables on rhs: "
- (map dest_Free (term_frees rhs) |> subtract (op =) lfrees
+ (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees
|> filter_out (is_fixed o fst));
case AList.lookup (op =) rec_fns fname of
NONE =>