moved term subst functions to TermSubst;

--- a/src/Pure/Isar/rule_insts.ML	Tue Sep 12 12:12:39 2006 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Tue Sep 12 12:12:46 2006 +0200
@@ -40,7 +40,7 @@
   end;
 
 fun instantiate inst =
-  Term.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
+  TermSubst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
   Envir.beta_norm;
 
 fun make_instT f v =
@@ -88,7 +88,7 @@
       end;
 
     val type_insts1 = map readT type_insts;
-    val instT1 = Term.instantiateT type_insts1;
+    val instT1 = TermSubst.instantiateT type_insts1;
     val vars1 = map (apsnd instT1) vars;
 
 

--- a/src/Pure/consts.ML	Tue Sep 12 12:12:39 2006 +0200
+++ b/src/Pure/consts.ML	Tue Sep 12 12:12:46 2006 +0200
@@ -177,7 +177,7 @@
   let
     val declT = declaration consts c;
     val vars = map Term.dest_TVar (typargs consts (c, declT));
-  in declT |> Term.instantiateT (vars ~~ Ts) end;
+  in declT |> TermSubst.instantiateT (vars ~~ Ts) end;
 
 
 

--- a/src/Pure/drule.ML	Tue Sep 12 12:12:39 2006 +0200
+++ b/src/Pure/drule.ML	Tue Sep 12 12:12:46 2006 +0200
@@ -396,7 +396,7 @@
   let
     val thy = Thm.theory_of_thm th;
     val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
-    val (instT, inst) = Term.zero_var_indexes_inst (Thm.full_prop_of th);
+    val (instT, inst) = TermSubst.zero_var_indexes_inst (Thm.full_prop_of th);
     val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
     val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
   in Thm.adjust_maxidx_thm ~1 (Thm.instantiate (cinstT, cinst) th) end;
@@ -914,7 +914,7 @@
     val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
     val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
     val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
-      let val T' = Term.instantiateT instT0 T
+      let val T' = TermSubst.instantiateT instT0 T
       in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
   in Thm.instantiate (instT, inst) th end;
 

--- a/src/Pure/proofterm.ML	Tue Sep 12 12:12:39 2006 +0200
+++ b/src/Pure/proofterm.ML	Tue Sep 12 12:12:46 2006 +0200
@@ -421,12 +421,12 @@
 
 (**** substitutions ****)
 
-fun del_conflicting_tvars envT T = Term.instantiateT
+fun del_conflicting_tvars envT T = TermSubst.instantiateT
   (map_filter (fn ixnS as (_, S) =>
      (Type.lookup (envT, ixnS); NONE) handle TYPE _ =>
         SOME (ixnS, TFree ("'dummy", S))) (typ_tvars T)) T;
 
-fun del_conflicting_vars env t = Term.instantiate
+fun del_conflicting_vars env t = TermSubst.instantiate
   (map_filter (fn ixnS as (_, S) =>
      (Type.lookup (type_env env, ixnS); NONE) handle TYPE _ =>
         SOME (ixnS, TFree ("'dummy", S))) (term_tvars t),
@@ -665,16 +665,16 @@
 
 fun generalize (tfrees, frees) idx =
   map_proof_terms_option
-    (Term.generalize_option (tfrees, frees) idx)
-    (Term.generalizeT_option tfrees idx);
+    (TermSubst.generalize_option (tfrees, frees) idx)
+    (TermSubst.generalizeT_option tfrees idx);
 
 
 (***** instantiation *****)
 
 fun instantiate (instT, inst) =
   map_proof_terms_option
-    (Term.instantiate_option (instT, map (apsnd remove_types) inst))
-    (Term.instantiateT_option instT);
+    (TermSubst.instantiate_option (instT, map (apsnd remove_types) inst))
+    (TermSubst.instantiateT_option instT);
 
 
 (***** lifting *****)

--- a/src/Pure/variable.ML	Tue Sep 12 12:12:39 2006 +0200
+++ b/src/Pure/variable.ML	Tue Sep 12 12:12:46 2006 +0200
@@ -322,19 +322,19 @@
 fun exportT_inst inner outer = #1 (export_inst inner outer);
 
 fun exportT_terms inner outer ts =
-  map (Term.generalize (exportT_inst (fold declare_type_occs ts inner) outer, [])
+  map (TermSubst.generalize (exportT_inst (fold declare_type_occs ts inner) outer, [])
     (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) ts;
 
 fun export_terms inner outer ts =
-  map (Term.generalize (export_inst (fold declare_type_occs ts inner) outer)
+  map (TermSubst.generalize (export_inst (fold declare_type_occs ts inner) outer)
     (fold Term.maxidx_term ts ~1 + 1)) ts;
 
 fun export_prf inner outer prf =
   let
     val insts = export_inst (declare_prf prf inner) outer;
     val idx = Proofterm.maxidx_proof prf ~1 + 1;
-    val gen_term = Term.generalize_option insts idx;
-    val gen_typ = Term.generalizeT_option (#1 insts) idx;
+    val gen_term = TermSubst.generalize_option insts idx;
+    val gen_typ = TermSubst.generalizeT_option (#1 insts) idx;
   in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
 
 fun gen_export inst inner outer ths =
@@ -359,18 +359,18 @@
   let
     val ren = if is_open then I else Name.internal;
     val (instT, ctxt') = importT_inst ts ctxt;
-    val vars = map (apsnd (Term.instantiateT instT)) (rev (fold Term.add_vars ts []));
+    val vars = map (apsnd (TermSubst.instantiateT instT)) (rev (fold Term.add_vars ts []));
     val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt';
     val inst = vars ~~ map Free (xs ~~ map #2 vars);
   in ((instT, inst), ctxt'') end;
 
 fun importT_terms ts ctxt =
   let val (instT, ctxt') = importT_inst ts ctxt
-  in (map (Term.instantiate (instT, [])) ts, ctxt') end;
+  in (map (TermSubst.instantiate (instT, [])) ts, ctxt') end;
 
 fun import_terms is_open ts ctxt =
   let val (inst, ctxt') = import_inst is_open ts ctxt
-  in (map (Term.instantiate inst) ts, ctxt') end;
+  in (map (TermSubst.instantiate inst) ts, ctxt') end;
 
 fun importT ths ctxt =
   let
@@ -472,6 +472,6 @@
     val occs' = type_occs_of ctxt';
     val types = Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else cons a) occs' [];
     val idx = fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1;
-  in map (Term.generalize (types, []) idx) ts end;
+  in map (TermSubst.generalize (types, []) idx) ts end;
 
 end;