moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
authorwenzelm
Wed Dec 31 18:53:19 2008 +0100 (2008-12-31)
changeset 292759fa69e3858d6
parent 29274 84e1729dda9c
child 29276 94b1ffec9201
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
use regular Term.add_XXX etc.;
src/Pure/Isar/locale.ML
src/Pure/type.ML
src/Tools/Compute_Oracle/linker.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Dec 31 18:53:18 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Dec 31 18:53:19 2008 +0100
     1.3 @@ -714,7 +714,7 @@
     1.4      val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
     1.5  
     1.6      fun inst_parms (i, ps) =
     1.7 -      List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
     1.8 +      List.foldr OldTerm.add_typ_tfrees [] (map_filter snd ps)
     1.9        |> map_filter (fn (a, S) =>
    1.10            let val T = Envir.norm_type unifier' (TVar ((a, i), S))
    1.11            in if T = TFree (a, S) then NONE else SOME (a, T) end)
    1.12 @@ -1791,10 +1791,11 @@
    1.13      val name = Sign.full_bname thy bname;
    1.14  
    1.15      val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
    1.16 -    val env = Term.add_term_free_names (body, []);
    1.17 +    val env = Term.add_free_names body [];
    1.18      val xs = filter (member (op =) env o #1) parms;
    1.19      val Ts = map #2 xs;
    1.20 -    val extraTs = (Term.term_tfrees body \\ List.foldr Term.add_typ_tfrees [] Ts)
    1.21 +    val extraTs =
    1.22 +      (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts [])
    1.23        |> Library.sort_wrt #1 |> map TFree;
    1.24      val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
    1.25  
    1.26 @@ -1949,8 +1950,8 @@
    1.27      val elemss = import_elemss @ body_elemss |>
    1.28        map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
    1.29  
    1.30 -    val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
    1.31 -      List.foldr Term.add_typ_tfrees [] (map snd parms);
    1.32 +    val extraTs = List.foldr OldTerm.add_term_tfrees [] exts' \\
    1.33 +      List.foldr OldTerm.add_typ_tfrees [] (map snd parms);
    1.34      val _ = if null extraTs then ()
    1.35        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
    1.36  
     2.1 --- a/src/Pure/type.ML	Wed Dec 31 18:53:18 2008 +0100
     2.2 +++ b/src/Pure/type.ML	Wed Dec 31 18:53:19 2008 +0100
     2.3 @@ -265,9 +265,9 @@
     2.4  (* no_tvars *)
     2.5  
     2.6  fun no_tvars T =
     2.7 -  (case typ_tvars T of [] => T
     2.8 +  (case Term.add_tvarsT T [] of [] => T
     2.9    | vs => raise TYPE ("Illegal schematic type variable(s): " ^
    2.10 -      commas_quote (map (Term.string_of_vname o #1) vs), [T], []));
    2.11 +      commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], []));
    2.12  
    2.13  
    2.14  (* varify *)
    2.15 @@ -307,8 +307,8 @@
    2.16  (*this sort of code could replace unvarifyT*)
    2.17  fun freeze_thaw_type T =
    2.18    let
    2.19 -    val used = add_typ_tfree_names (T, [])
    2.20 -    and tvars = map #1 (add_typ_tvars (T, []));
    2.21 +    val used = OldTerm.add_typ_tfree_names (T, [])
    2.22 +    and tvars = map #1 (OldTerm.add_typ_tvars (T, []));
    2.23      val (alist, _) = List.foldr new_name ([], used) tvars;
    2.24    in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
    2.25  
    2.26 @@ -316,8 +316,8 @@
    2.27  
    2.28  fun freeze_thaw t =
    2.29    let
    2.30 -    val used = it_term_types add_typ_tfree_names (t, [])
    2.31 -    and tvars = map #1 (it_term_types add_typ_tvars (t, []));
    2.32 +    val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
    2.33 +    and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
    2.34      val (alist, _) = List.foldr new_name ([], used) tvars;
    2.35    in
    2.36      (case alist of
     3.1 --- a/src/Tools/Compute_Oracle/linker.ML	Wed Dec 31 18:53:18 2008 +0100
     3.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Wed Dec 31 18:53:19 2008 +0100
     3.3 @@ -81,7 +81,7 @@
     3.4  
     3.5  datatype instances = Instances of unit ConsttabModTy.table * Type.tyenv Consttab.table Consttab.table * constant list list * unit Substtab.table
     3.6  
     3.7 -fun is_polymorphic (Constant (_, _, ty)) = not (null (typ_tvars ty))
     3.8 +fun is_polymorphic (Constant (_, _, ty)) = not (null (Term.add_tvarsT ty []))
     3.9  
    3.10  fun distinct_constants cs =
    3.11      Consttab.keys (fold (fn c => Consttab.update (c, ())) cs Consttab.empty)
    3.12 @@ -90,7 +90,7 @@
    3.13      let
    3.14          val cs = distinct_constants (filter is_polymorphic cs)
    3.15          val old_cs = cs
    3.16 -(*      fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (typ_tvars ty) tab
    3.17 +(*      fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (OldTerm.typ_tvars ty) tab
    3.18          val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
    3.19          fun tvars_of ty = collect_tvars ty Typtab.empty
    3.20          val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs
    3.21 @@ -262,10 +262,10 @@
    3.22  let
    3.23      val (left, right) = collect_consts_of_thm th
    3.24      val polycs = filter Linker.is_polymorphic left
    3.25 -    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
    3.26 +    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
    3.27      fun check_const (c::cs) cs' =
    3.28          let
    3.29 -            val tvars = typ_tvars (Linker.typ_of_constant c)
    3.30 +            val tvars = OldTerm.typ_tvars (Linker.typ_of_constant c)
    3.31              val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
    3.32          in
    3.33              if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"