# HG changeset patch # User wenzelm # Date 1247177436 -7200 # Node ID 354708e9e85ce4db6474257ff39c3d5ac5c6727f # Parent 09f65e860bdb62a9ccfb4b75f1cfda1ed29e8bff# Parent c7c1d545007e2a9d50021e78917c3b5c07fceea5 merged diff -r 09f65e860bdb -r 354708e9e85c src/FOL/FOL.thy --- a/src/FOL/FOL.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/FOL.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/FOL.thy - ID: $Id$ Author: Lawrence C Paulson and Markus Wenzel *) diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ROOT.ML --- a/src/FOL/ROOT.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ROOT.ML Fri Jul 10 00:10:36 2009 +0200 @@ -1,7 +1,3 @@ -(* Title: FOL/ROOT.ML - ID: $Id$ - -First-Order Logic with Natural Deduction. -*) +(* First-Order Logic with Natural Deduction *) use_thy "FOL"; diff -r 09f65e860bdb -r 354708e9e85c src/FOL/cladata.ML --- a/src/FOL/cladata.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/cladata.ML Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/cladata.ML - ID: $Id$ Author: Tobias Nipkow Copyright 1996 University of Cambridge diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Classical.thy --- a/src/FOL/ex/Classical.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Classical.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ -(* Title: FOL/ex/Classical - ID: $Id$ +(* Title: FOL/ex/Classical.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge *) diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/First_Order_Logic.thy --- a/src/FOL/ex/First_Order_Logic.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/First_Order_Logic.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/First_Order_Logic.thy - ID: $Id$ Author: Markus Wenzel, TU Munich *) diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Foundation.thy --- a/src/FOL/ex/Foundation.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Foundation.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ -(* Title: FOL/ex/Foundation.ML - ID: $Id$ +(* Title: FOL/ex/Foundation.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *) diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/If.thy --- a/src/FOL/ex/If.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/If.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/If.ML - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *) diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Intro.thy --- a/src/FOL/ex/Intro.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Intro.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/Intro.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Intuitionistic.thy --- a/src/FOL/ex/Intuitionistic.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Intuitionistic.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,12 +1,13 @@ -(* Title: FOL/ex/Intuitionistic - ID: $Id$ +(* Title: FOL/ex/Intuitionistic.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *) -header{*Intuitionistic First-Order Logic*} +header {* Intuitionistic First-Order Logic *} -theory Intuitionistic imports IFOL begin +theory Intuitionistic +imports IFOL +begin (* Single-step ML commands: @@ -422,4 +423,3 @@ end - diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Miniscope.thy --- a/src/FOL/ex/Miniscope.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Miniscope.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/Miniscope.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Nat.thy --- a/src/FOL/ex/Nat.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Nat.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/Nat.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Natural_Numbers.thy --- a/src/FOL/ex/Natural_Numbers.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Natural_Numbers.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,11 +1,12 @@ (* Title: FOL/ex/Natural_Numbers.thy - ID: $Id$ Author: Markus Wenzel, TU Munich *) header {* Natural numbers *} -theory Natural_Numbers imports FOL begin +theory Natural_Numbers +imports FOL +begin text {* Theory of the natural numbers: Peano's axioms, primitive recursion. diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Prolog.thy --- a/src/FOL/ex/Prolog.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Prolog.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ -(* Title: FOL/ex/prolog.thy - ID: $Id$ +(* Title: FOL/ex/Prolog.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Propositional_Cla.thy --- a/src/FOL/ex/Propositional_Cla.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Propositional_Cla.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/Propositional_Cla.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *) diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Propositional_Int.thy --- a/src/FOL/ex/Propositional_Int.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Propositional_Int.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/Propositional_Int.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *) diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Quantifiers_Cla.thy --- a/src/FOL/ex/Quantifiers_Cla.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Quantifiers_Cla.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/Quantifiers_Int.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *) diff -r 09f65e860bdb -r 354708e9e85c src/FOL/ex/Quantifiers_Int.thy --- a/src/FOL/ex/Quantifiers_Int.thy Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/ex/Quantifiers_Int.thy Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/ex/Quantifiers_Int.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *) diff -r 09f65e860bdb -r 354708e9e85c src/FOL/fologic.ML --- a/src/FOL/fologic.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/fologic.ML Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/fologic.ML - ID: $Id$ Author: Lawrence C Paulson Abstract syntax operations for FOL. diff -r 09f65e860bdb -r 354708e9e85c src/FOL/intprover.ML --- a/src/FOL/intprover.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/intprover.ML Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ -(* Title: FOL/int-prover - ID: $Id$ +(* Title: FOL/intprover.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge diff -r 09f65e860bdb -r 354708e9e85c src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/FOL/simpdata.ML Fri Jul 10 00:10:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: FOL/simpdata.ML - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge diff -r 09f65e860bdb -r 354708e9e85c src/HOL/Library/Library/ROOT.ML --- a/src/HOL/Library/Library/ROOT.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/HOL/Library/Library/ROOT.ML Fri Jul 10 00:10:36 2009 +0200 @@ -1,3 +1,1 @@ -(* $Id$ *) - use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"]; diff -r 09f65e860bdb -r 354708e9e85c src/HOL/Library/Library/document/root.tex --- a/src/HOL/Library/Library/document/root.tex Thu Jul 09 23:05:59 2009 +0200 +++ b/src/HOL/Library/Library/document/root.tex Fri Jul 10 00:10:36 2009 +0200 @@ -1,6 +1,3 @@ - -% $Id$ - \documentclass[11pt,a4paper]{article} \usepackage{ifthen} \usepackage[latin1]{inputenc} diff -r 09f65e860bdb -r 354708e9e85c src/HOL/Library/README.html --- a/src/HOL/Library/README.html Thu Jul 09 23:05:59 2009 +0200 +++ b/src/HOL/Library/README.html Fri Jul 10 00:10:36 2009 +0200 @@ -1,7 +1,5 @@ - - diff -r 09f65e860bdb -r 354708e9e85c src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/Isar/expression.ML Fri Jul 10 00:10:36 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 09f65e860bdb -r 354708e9e85c src/Pure/Isar/rule_insts.ML --- a/src/Pure/Isar/rule_insts.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/Isar/rule_insts.ML Fri Jul 10 00:10:36 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 09f65e860bdb -r 354708e9e85c src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/Isar/theory_target.ML Fri Jul 10 00:10:36 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 09f65e860bdb -r 354708e9e85c src/Pure/consts.ML --- a/src/Pure/consts.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/consts.ML Fri Jul 10 00:10:36 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 09f65e860bdb -r 354708e9e85c src/Pure/drule.ML --- a/src/Pure/drule.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/drule.ML Fri Jul 10 00:10:36 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 09f65e860bdb -r 354708e9e85c src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/more_thm.ML Fri Jul 10 00:10:36 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 09f65e860bdb -r 354708e9e85c src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/proofterm.ML Fri Jul 10 00:10:36 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 09f65e860bdb -r 354708e9e85c src/Pure/term_ord.ML --- a/src/Pure/term_ord.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/term_ord.ML Fri Jul 10 00:10:36 2009 +0200 @@ -205,5 +205,6 @@ end; structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_ord); +structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord); structure Typtab = Table(type key = typ val ord = TermOrd.typ_ord); structure Termtab = Table(type key = term val ord = TermOrd.fast_term_ord); diff -r 09f65e860bdb -r 354708e9e85c src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/term_subst.ML Fri Jul 10 00:10:36 2009 +0200 @@ -1,11 +1,15 @@ (* Title: Pure/term_subst.ML Author: Makarius -Efficient term substitution -- avoids copying. +Efficient type/term substitution -- avoids copying. *) signature TERM_SUBST = sig + val map_atypsT_option: (typ -> typ option) -> typ -> typ option + val map_atyps_option: (typ -> typ option) -> term -> term option + val map_types_option: (typ -> typ option) -> term -> term option + val map_aterms_option: (term -> term option) -> term -> term option val generalize: string list * string list -> int -> term -> term val generalizeT: string list -> int -> typ -> typ val generalize_option: string list * string list -> int -> term -> term option @@ -25,15 +29,67 @@ ((indexname * sort) * typ) list * ((indexname * typ) * term) list end; -structure TermSubst: TERM_SUBST = +structure Term_Subst: TERM_SUBST = struct +(* indication of same result *) + +exception SAME; + +fun same_fn f x = + (case f x of + NONE => raise SAME + | SOME y => y); + +fun option_fn f x = + SOME (f x) handle SAME => NONE; + + +(* generic mapping *) + +local + +fun map_atypsT_same f = + let + fun typ (Type (a, Ts)) = Type (a, typs Ts) + | typ T = f T + and typs (T :: Ts) = (typ T :: (typs Ts handle SAME => Ts) handle SAME => T :: typs Ts) + | typs [] = raise SAME; + in typ end; + +fun map_types_same f = + let + fun term (Const (a, T)) = Const (a, f T) + | term (Free (a, T)) = Free (a, f T) + | term (Var (v, T)) = Var (v, f T) + | term (Bound _) = raise SAME + | term (Abs (x, T, t)) = + (Abs (x, f T, term t handle SAME => t) + handle SAME => Abs (x, T, term t)) + | term (t $ u) = (term t $ (term u handle SAME => u) handle SAME => t $ term u); + in term end; + +fun map_aterms_same f = + let + fun term (Abs (x, T, t)) = Abs (x, T, term t) + | term (t $ u) = (term t $ (term u handle SAME => u) handle SAME => t $ term u) + | term a = f a; + in term end; + +in + +val map_atypsT_option = option_fn o map_atypsT_same o same_fn; +val map_atyps_option = option_fn o map_types_same o map_atypsT_same o same_fn; +val map_types_option = option_fn o map_types_same o same_fn; +val map_aterms_option = option_fn o map_aterms_same o same_fn; + +end; + + (* generalization of fixed variables *) local -exception SAME; - fun generalizeT_same [] _ _ = raise SAME | generalizeT_same tfrees idx ty = let @@ -84,8 +140,6 @@ fun no_indexes1 inst = map no_index inst; fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2); -exception SAME; - fun instantiateT_same maxidx instT ty = let fun maxify i = if i > ! maxidx then maxidx := i else (); diff -r 09f65e860bdb -r 354708e9e85c src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/thm.ML Fri Jul 10 00:10:36 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 09f65e860bdb -r 354708e9e85c src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/type_infer.ML Fri Jul 10 00:10:36 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 09f65e860bdb -r 354708e9e85c src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Pure/variable.ML Fri Jul 10 00:10:36 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 09f65e860bdb -r 354708e9e85c src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Tools/Code/code_preproc.ML Fri Jul 10 00:10:36 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) diff -r 09f65e860bdb -r 354708e9e85c src/Tools/Compute_Oracle/compute.ML --- a/src/Tools/Compute_Oracle/compute.ML Thu Jul 09 23:05:59 2009 +0200 +++ b/src/Tools/Compute_Oracle/compute.ML Fri Jul 10 00:10:36 2009 +0200 @@ -167,8 +167,6 @@ | machine_of_prog (ProgHaskell _) = HASKELL | machine_of_prog (ProgSML _) = SML -structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord) - type naming = int -> string fun default_naming i = "v_" ^ Int.toString i