--- a/src/HOL/Matrix/cplex/matrixlp.ML Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Matrix/cplex/matrixlp.ML Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Matrix/cplex/matrixlp.ML
- ID: $Id$
Author: Steven Obua
*)
@@ -20,7 +19,7 @@
fun inst_real thm =
let val certT = ctyp_of (Thm.theory_of_thm thm) in
standard (Thm.instantiate
- ([(certT (TVar (hd (term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
+ ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
end
local
@@ -58,7 +57,7 @@
let
val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
- val v = TVar (hd (sort ord (term_tvars (prop_of thm))))
+ val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
in
standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
end