# HG changeset patch
# User wenzelm
# Date 1247172492 -7200
# Node ID e03059ae2d8299fb4677cbe7d884a949613ea29b
# Parent  17414e2736f406d6426c7d45810229e7fe7e191f
renamed structure TermSubst to Term_Subst;

diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -492,7 +492,7 @@
 
     val export = Variable.export_morphism goal_ctxt context;
     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
-    val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
+    val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
     val exp_typ = Logic.type_map exp_term;
     val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
   in ((propss, deps, export'), goal_ctxt) end;
diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -58,7 +58,7 @@
   end;
 
 fun instantiate inst =
-  TermSubst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
+  Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
   Envir.beta_norm;
 
 fun make_instT f v =
@@ -124,7 +124,7 @@
       end;
 
     val type_insts1 = map readT type_insts;
-    val instT1 = TermSubst.instantiateT type_insts1;
+    val instT1 = Term_Subst.instantiateT type_insts1;
     val vars1 = map (apsnd instT1) vars;
 
 
diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/Isar/theory_target.ML
--- 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*)
diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/consts.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -215,7 +215,7 @@
     val vars = map Term.dest_TVar (typargs consts (c, declT));
     val inst = vars ~~ Ts handle UnequalLengths =>
       raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
-  in declT |> TermSubst.instantiateT inst end;
+  in declT |> Term_Subst.instantiateT inst end;
 
 
 
diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/drule.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -278,7 +278,7 @@
       let
         val thy = Theory.merge_list (map Thm.theory_of_thm ths);
         val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
-        val (instT, inst) = TermSubst.zero_var_indexes_inst (map Thm.full_prop_of ths);
+        val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
         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 map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/more_thm.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -274,7 +274,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' = TermSubst.instantiateT instT0 T
+      let val T' = Term_Subst.instantiateT instT0 T
       in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
   in Thm.instantiate (instT, inst) th end;
 
diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/proofterm.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -441,12 +441,12 @@
 
 (**** substitutions ****)
 
-fun del_conflicting_tvars envT T = TermSubst.instantiateT
+fun del_conflicting_tvars envT T = Term_Subst.instantiateT
   (map_filter (fn ixnS as (_, S) =>
      (Type.lookup envT ixnS; NONE) handle TYPE _ =>
         SOME (ixnS, TFree ("'dummy", S))) (OldTerm.typ_tvars T)) T;
 
-fun del_conflicting_vars env t = TermSubst.instantiate
+fun del_conflicting_vars env t = Term_Subst.instantiate
   (map_filter (fn ixnS as (_, S) =>
      (Type.lookup (type_env env) ixnS; NONE) handle TYPE _ =>
         SOME (ixnS, TFree ("'dummy", S))) (OldTerm.term_tvars t),
@@ -689,16 +689,16 @@
 
 fun generalize (tfrees, frees) idx =
   map_proof_terms_option
-    (TermSubst.generalize_option (tfrees, frees) idx)
-    (TermSubst.generalizeT_option tfrees idx);
+    (Term_Subst.generalize_option (tfrees, frees) idx)
+    (Term_Subst.generalizeT_option tfrees idx);
 
 
 (***** instantiation *****)
 
 fun instantiate (instT, inst) =
   map_proof_terms_option
-    (TermSubst.instantiate_option (instT, map (apsnd remove_types) inst))
-    (TermSubst.instantiateT_option instT);
+    (Term_Subst.instantiate_option (instT, map (apsnd remove_types) inst))
+    (Term_Subst.instantiateT_option instT);
 
 
 (***** lifting *****)
diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/term_subst.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -25,7 +25,7 @@
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list
 end;
 
-structure TermSubst: TERM_SUBST =
+structure Term_Subst: TERM_SUBST =
 struct
 
 (* generalization of fixed variables *)
diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/thm.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -995,7 +995,7 @@
         val _ = exists bad_term hyps andalso
           raise THM ("generalize: variable free in assumptions", 0, [th]);
 
-        val gen = TermSubst.generalize (tfrees, frees) idx;
+        val gen = Term_Subst.generalize (tfrees, frees) idx;
         val prop' = gen prop;
         val tpairs' = map (pairself gen) tpairs;
         val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
@@ -1066,7 +1066,7 @@
         val Thm (der, {thy_ref, hyps, shyps, tpairs, prop, ...}) = th;
         val (inst', (instT', (thy_ref', shyps'))) =
           (thy_ref, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT;
-        val subst = TermSubst.instantiate_maxidx (instT', inst');
+        val subst = Term_Subst.instantiate_maxidx (instT', inst');
         val (prop', maxidx1) = subst prop ~1;
         val (tpairs', maxidx') =
           fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
@@ -1088,8 +1088,8 @@
         val Cterm {thy_ref, t, T, sorts, ...} = ct;
         val (inst', (instT', (thy_ref', sorts'))) =
           (thy_ref, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT;
-        val subst = TermSubst.instantiate_maxidx (instT', inst');
-        val substT = TermSubst.instantiateT_maxidx instT';
+        val subst = Term_Subst.instantiate_maxidx (instT', inst');
+        val substT = Term_Subst.instantiateT_maxidx instT';
         val (t', maxidx1) = subst t ~1;
         val (T', maxidx') = substT T maxidx1;
       in Cterm {thy_ref = thy_ref', t = t', T = T', sorts = sorts', maxidx = maxidx'} end
diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/type_infer.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -64,7 +64,7 @@
       else (inst, used);
     val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
     val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
-  in (map o map_types) (TermSubst.instantiateT inst) ts end;
+  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
 
 
 
diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/variable.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -360,14 +360,14 @@
 fun exportT_terms inner outer =
   let val mk_tfrees = exportT_inst inner outer in
     fn ts => ts |> map
-      (TermSubst.generalize (mk_tfrees ts, [])
+      (Term_Subst.generalize (mk_tfrees ts, [])
         (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1))
   end;
 
 fun export_terms inner outer =
   let val (mk_tfrees, tfrees) = export_inst inner outer in
     fn ts => ts |> map
-      (TermSubst.generalize (mk_tfrees ts, tfrees)
+      (Term_Subst.generalize (mk_tfrees ts, tfrees)
         (fold Term.maxidx_term ts ~1 + 1))
   end;
 
@@ -376,8 +376,8 @@
     val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
     val tfrees = mk_tfrees [];
     val idx = Proofterm.maxidx_proof prf ~1 + 1;
-    val gen_term = TermSubst.generalize_option (tfrees, frees) idx;
-    val gen_typ = TermSubst.generalizeT_option tfrees idx;
+    val gen_term = Term_Subst.generalize_option (tfrees, frees) idx;
+    val gen_typ = Term_Subst.generalizeT_option tfrees idx;
   in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
 
 
@@ -411,18 +411,18 @@
   let
     val ren = Name.clean #> (if is_open then I else Name.internal);
     val (instT, ctxt') = importT_inst ts ctxt;
-    val vars = map (apsnd (TermSubst.instantiateT instT)) (rev (fold Term.add_vars ts []));
+    val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (fold Term.add_vars ts []));
     val (xs, ctxt'') = variant_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 (TermSubst.instantiate (instT, [])) ts, ctxt') end;
+  in (map (Term_Subst.instantiate (instT, [])) ts, ctxt') end;
 
 fun import_terms is_open ts ctxt =
   let val (inst, ctxt') = import_inst is_open ts ctxt
-  in (map (TermSubst.instantiate inst) ts, ctxt') end;
+  in (map (Term_Subst.instantiate inst) ts, ctxt') end;
 
 fun importT ths ctxt =
   let
@@ -527,9 +527,9 @@
     val idx = maxidx_of ctxt' + 1;
     val Ts' = (fold o fold_types o fold_atyps)
       (fn T as TFree _ =>
-          (case TermSubst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
+          (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
         | _ => I) ts [];
-    val ts' = map (TermSubst.generalize (types, []) idx) ts;
+    val ts' = map (Term_Subst.generalize (types, []) idx) ts;
   in (rev Ts', ts') end;
 
 fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts);
diff -r 17414e2736f4 -r e03059ae2d82 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -224,7 +224,7 @@
 
 fun default_typscheme_of thy c =
   let
-    val ty = (snd o dest_Const o TermSubst.zero_var_indexes o curry Const c
+    val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c
       o Type.strip_sorts o Sign.the_const_type thy) c;
   in case AxClass.class_of_param thy c
    of SOME class => ([(Name.aT, [class])], ty)