--- a/src/Pure/Isar/theory_target.ML Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML Thu Jul 09 22:48:12 2009 +0200
@@ -130,7 +130,7 @@
val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
val inst = filter (is_Var o fst) (vars ~~ frees);
val cinstT = map (pairself certT o apfst TVar) instT;
- val cinst = map (pairself (cert o Term.map_types (TermSubst.instantiateT instT))) inst;
+ val cinst = map (pairself (cert o Term.map_types (Term_Subst.instantiateT instT))) inst;
val result' = Thm.instantiate (cinstT, cinst) result;
(*import assumes/defines*)