src/HOL/Tools/old_primrec_package.ML
changeset 29266 4a478f9d2847
parent 28703 aef727ef30e5
child 29276 94b1ffec9201
--- a/src/HOL/Tools/old_primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Tools/old_primrec_package.ML
-    ID:         $Id$
-    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 datatypes by primitive recursion.
 *)
@@ -58,7 +58,7 @@
 fun process_eqn thy eq rec_fns =
   let
     val (lhs, rhs) =
-      if null (term_vars eq) then
+      if null (Term.add_vars eq []) then
         HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
         handle TERM _ => raise RecError "not a proper equation"
       else raise RecError "illegal schematic variable(s)";
@@ -91,7 +91,7 @@
     else
      (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
       check_vars "extra variables on rhs: "
-        (map dest_Free (term_frees rhs) \\ lfrees);
+        (map dest_Free (OldTerm.term_frees rhs) \\ lfrees);
       case AList.lookup (op =) rec_fns fnameT of
         NONE =>
           (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns