--- 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;
--- 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;
--- 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*)
--- 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;
--- 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;
--- 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;
--- 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 *****)
--- 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 *)
--- 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
--- 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;
--- 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);
--- 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)