# HG changeset patch # User wenzelm # Date 1158055966 -7200 # Node ID 073a5ed7dd71b04441e3c1522a02ead074e55a1f # Parent 8182d961c7cc6c7c2f93b4590b28781c11fea005 moved term subst functions to TermSubst; diff -r 8182d961c7cc -r 073a5ed7dd71 src/Pure/Isar/rule_insts.ML --- 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; diff -r 8182d961c7cc -r 073a5ed7dd71 src/Pure/consts.ML --- 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; diff -r 8182d961c7cc -r 073a5ed7dd71 src/Pure/drule.ML --- 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; diff -r 8182d961c7cc -r 073a5ed7dd71 src/Pure/proofterm.ML --- 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 *****) diff -r 8182d961c7cc -r 073a5ed7dd71 src/Pure/variable.ML --- 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;