--- a/src/Pure/term_subst.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/term_subst.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/term_subst.ML
- ID: $Id$
Author: Makarius
Efficient term substitution -- avoids copying.
@@ -163,9 +162,9 @@
fun zero_var_indexes_inst ts =
let
- val tvars = sort Term.tvar_ord (fold Term.add_tvars ts []);
+ val tvars = sort TermOrd.tvar_ord (fold Term.add_tvars ts []);
val instT = map (apsnd TVar) (zero_var_inst tvars);
- val vars = sort Term.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
+ val vars = sort TermOrd.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
val inst = map (apsnd Var) (zero_var_inst vars);
in (instT, inst) end;