# HG changeset patch # User wenzelm # Date 1230745999 -3600 # Node ID 9fa69e3858d6bb1bd663e90ba543df6637bf745d # Parent 84e1729dda9c62b0f274903843c562fab322d9bc moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use regular Term.add_XXX etc.; diff -r 84e1729dda9c -r 9fa69e3858d6 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Dec 31 18:53:18 2008 +0100 +++ b/src/Pure/Isar/locale.ML Wed Dec 31 18:53:19 2008 +0100 @@ -714,7 +714,7 @@ val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier; fun inst_parms (i, ps) = - List.foldr Term.add_typ_tfrees [] (map_filter snd ps) + List.foldr OldTerm.add_typ_tfrees [] (map_filter snd ps) |> map_filter (fn (a, S) => let val T = Envir.norm_type unifier' (TVar ((a, i), S)) in if T = TFree (a, S) then NONE else SOME (a, T) end) @@ -1791,10 +1791,11 @@ val name = Sign.full_bname thy bname; val (body, bodyT, body_eq) = atomize_spec thy norm_ts; - val env = Term.add_term_free_names (body, []); + val env = Term.add_free_names body []; val xs = filter (member (op =) env o #1) parms; val Ts = map #2 xs; - val extraTs = (Term.term_tfrees body \\ List.foldr Term.add_typ_tfrees [] Ts) + val extraTs = + (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts []) |> Library.sort_wrt #1 |> map TFree; val predT = map Term.itselfT extraTs ---> Ts ---> bodyT; @@ -1949,8 +1950,8 @@ val elemss = import_elemss @ body_elemss |> map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE); - val extraTs = List.foldr Term.add_term_tfrees [] exts' \\ - List.foldr Term.add_typ_tfrees [] (map snd parms); + val extraTs = List.foldr OldTerm.add_term_tfrees [] exts' \\ + List.foldr OldTerm.add_typ_tfrees [] (map snd parms); val _ = if null extraTs then () else warning ("Additional type variable(s) in locale specification " ^ quote bname); diff -r 84e1729dda9c -r 9fa69e3858d6 src/Pure/type.ML --- a/src/Pure/type.ML Wed Dec 31 18:53:18 2008 +0100 +++ b/src/Pure/type.ML Wed Dec 31 18:53:19 2008 +0100 @@ -265,9 +265,9 @@ (* no_tvars *) fun no_tvars T = - (case typ_tvars T of [] => T + (case Term.add_tvarsT T [] of [] => T | vs => raise TYPE ("Illegal schematic type variable(s): " ^ - commas_quote (map (Term.string_of_vname o #1) vs), [T], [])); + commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], [])); (* varify *) @@ -307,8 +307,8 @@ (*this sort of code could replace unvarifyT*) fun freeze_thaw_type T = let - val used = add_typ_tfree_names (T, []) - and tvars = map #1 (add_typ_tvars (T, [])); + val used = OldTerm.add_typ_tfree_names (T, []) + and tvars = map #1 (OldTerm.add_typ_tvars (T, [])); val (alist, _) = List.foldr new_name ([], used) tvars; in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end; @@ -316,8 +316,8 @@ fun freeze_thaw t = let - val used = it_term_types add_typ_tfree_names (t, []) - and tvars = map #1 (it_term_types add_typ_tvars (t, [])); + val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, []) + and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, [])); val (alist, _) = List.foldr new_name ([], used) tvars; in (case alist of diff -r 84e1729dda9c -r 9fa69e3858d6 src/Tools/Compute_Oracle/linker.ML --- a/src/Tools/Compute_Oracle/linker.ML Wed Dec 31 18:53:18 2008 +0100 +++ b/src/Tools/Compute_Oracle/linker.ML Wed Dec 31 18:53:19 2008 +0100 @@ -81,7 +81,7 @@ datatype instances = Instances of unit ConsttabModTy.table * Type.tyenv Consttab.table Consttab.table * constant list list * unit Substtab.table -fun is_polymorphic (Constant (_, _, ty)) = not (null (typ_tvars ty)) +fun is_polymorphic (Constant (_, _, ty)) = not (null (Term.add_tvarsT ty [])) fun distinct_constants cs = Consttab.keys (fold (fn c => Consttab.update (c, ())) cs Consttab.empty) @@ -90,7 +90,7 @@ let val cs = distinct_constants (filter is_polymorphic cs) val old_cs = cs -(* fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (typ_tvars ty) tab +(* fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (OldTerm.typ_tvars ty) tab val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty)) fun tvars_of ty = collect_tvars ty Typtab.empty val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs @@ -262,10 +262,10 @@ let val (left, right) = collect_consts_of_thm th val polycs = filter Linker.is_polymorphic left - val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty + val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (OldTerm.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty fun check_const (c::cs) cs' = let - val tvars = typ_tvars (Linker.typ_of_constant c) + val tvars = OldTerm.typ_tvars (Linker.typ_of_constant c) val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false in if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"