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/Pure/old_term.ML
changeset 39687 4e9b6ada3a21
parent 37783 95aa0afcb240 
--- a/src/Pure/old_term.ML	Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/old_term.ML	Fri Sep 24 15:53:13 2010 +0200
@@ -75,7 +75,7 @@
 
 (*Accumulates the Vars in the term, suppressing duplicates.*)
 fun add_term_vars (t, vars: term list) = case t of
-    Var   _ => OrdList.insert Term_Ord.term_ord t vars
+    Var   _ => Ord_List.insert Term_Ord.term_ord t vars
   | Abs (_,_,body) => add_term_vars(body,vars)
   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   | _ => vars;
@@ -84,7 +84,7 @@
 
 (*Accumulates the Frees in the term, suppressing duplicates.*)
 fun add_term_frees (t, frees: term list) = case t of
-    Free   _ => OrdList.insert Term_Ord.term_ord t frees
+    Free   _ => Ord_List.insert Term_Ord.term_ord t frees
   | Abs (_,_,body) => add_term_frees(body,frees)
   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   | _ => frees;
isabelle