Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/primrec_package.ML
changeset 29265 5b4247055bd7
parent 29006 abe0f11cfa4e
child 29276 94b1ffec9201 
--- a/src/HOL/Tools/primrec_package.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -69,7 +69,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 =>
isabelle