use regular Term.add_XXX etc.;
authorwenzelm
Wed Dec 31 18:53:17 2008 +0100 (2008-12-31)
changeset 29272fb3ccf499df5
parent 29271 1d685baea08e
child 29273 285c00993bc2
use regular Term.add_XXX etc.;
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/typecopy_package.ML
src/Pure/Isar/expression.ML
src/Pure/tctical.ML
src/Pure/thm.ML
src/Tools/code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Wed Dec 31 18:53:16 2008 +0100
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Wed Dec 31 18:53:17 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Tools/recfun_codegen.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Stefan Berghofer, TU Muenchen
     1.7  
     1.8  Code generator for recursive functions.
     1.9 @@ -46,7 +45,7 @@
    1.10    | expand_eta thy (thms as thm :: _) =
    1.11        let
    1.12          val (_, ty) = Code_Unit.const_typ_eqn thm;
    1.13 -      in if (null o Term.typ_tvars) ty orelse (null o fst o strip_type) ty
    1.14 +      in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty
    1.15          then thms
    1.16          else map (Code_Unit.expand_eta thy 1) thms
    1.17        end;
     2.1 --- a/src/HOL/Tools/refute.ML	Wed Dec 31 18:53:16 2008 +0100
     2.2 +++ b/src/HOL/Tools/refute.ML	Wed Dec 31 18:53:17 2008 +0100
     2.3 @@ -790,7 +790,7 @@
     2.4        (* replace the (at most one) schematic type variable in each axiom *)
     2.5        (* by the actual type 'T'                                          *)
     2.6        val monomorphic_class_axioms = map (fn (axname, ax) =>
     2.7 -        (case Term.term_tvars ax of
     2.8 +        (case Term.add_tvars ax [] of
     2.9            [] =>
    2.10            (axname, ax)
    2.11          | [(idx, S)] =>
    2.12 @@ -942,16 +942,13 @@
    2.13  (*               and all mutually recursive IDTs are considered.             *)
    2.14  (* ------------------------------------------------------------------------- *)
    2.15  
    2.16 -  (* theory -> Term.term -> Term.typ list *)
    2.17 -
    2.18    fun ground_types thy t =
    2.19    let
    2.20 -    (* Term.typ * Term.typ list -> Term.typ list *)
    2.21 -    fun collect_types (T, acc) =
    2.22 +    fun collect_types T acc =
    2.23        (case T of
    2.24 -        Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc))
    2.25 +        Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
    2.26        | Type ("prop", [])      => acc
    2.27 -      | Type ("set", [T1])     => collect_types (T1, acc)
    2.28 +      | Type ("set", [T1])     => collect_types T1 acc
    2.29        | Type (s, Ts)           =>
    2.30          (case DatatypePackage.get_datatype thy s of
    2.31            SOME info =>  (* inductive datatype *)
    2.32 @@ -976,9 +973,9 @@
    2.33              in
    2.34                case d of
    2.35                  DatatypeAux.DtTFree _ =>
    2.36 -                collect_types (dT, acc)
    2.37 +                collect_types dT acc
    2.38                | DatatypeAux.DtType (_, ds) =>
    2.39 -                collect_types (dT, foldr collect_dtyp acc ds)
    2.40 +                collect_types dT (foldr collect_dtyp acc ds)
    2.41                | DatatypeAux.DtRec i =>
    2.42                  if dT mem acc then
    2.43                    acc  (* prevent infinite recursion *)
    2.44 @@ -1008,11 +1005,11 @@
    2.45          | NONE =>
    2.46            (* not an inductive datatype, e.g. defined via "typedef" or *)
    2.47            (* "typedecl"                                               *)
    2.48 -          insert (op =) T (foldr collect_types acc Ts))
    2.49 +          insert (op =) T (fold collect_types Ts acc))
    2.50        | TFree _                => insert (op =) T acc
    2.51        | TVar _                 => insert (op =) T acc)
    2.52    in
    2.53 -    it_term_types collect_types (t, [])
    2.54 +    fold_types collect_types t []
    2.55    end;
    2.56  
    2.57  (* ------------------------------------------------------------------------- *)
    2.58 @@ -1287,7 +1284,7 @@
    2.59      (* terms containing them (their logical meaning is that there EXISTS a *)
    2.60      (* type s.t. ...; to refute such a formula, we would have to show that *)
    2.61      (* for ALL types, not ...)                                             *)
    2.62 -    val _ = null (term_tvars t) orelse
    2.63 +    val _ = null (Term.add_tvars t []) orelse
    2.64        error "Term to be refuted contains schematic type variables"
    2.65  
    2.66      (* existential closure over schematic variables *)
     3.1 --- a/src/HOL/Tools/res_reconstruct.ML	Wed Dec 31 18:53:16 2008 +0100
     3.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Wed Dec 31 18:53:17 2008 +0100
     3.3 @@ -405,7 +405,7 @@
     3.4  fun add_wanted_prfline ctxt ((lno, t, []), (nlines, lines)) =
     3.5        (nlines, (lno, t, []) :: lines)   (*conjecture clauses must be kept*)
     3.6    | add_wanted_prfline ctxt ((lno, t, deps), (nlines, lines)) =
     3.7 -      if eq_types t orelse not (null (term_tvars t)) orelse
     3.8 +      if eq_types t orelse not (null (Term.add_tvars t [])) orelse
     3.9           exists_subterm bad_free t orelse
    3.10           (not (null lines) andalso   (*final line can't be deleted for these reasons*)
    3.11            (length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0))   
     4.1 --- a/src/HOL/Tools/typecopy_package.ML	Wed Dec 31 18:53:16 2008 +0100
     4.2 +++ b/src/HOL/Tools/typecopy_package.ML	Wed Dec 31 18:53:17 2008 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOL/Tools/typecopy_package.ML
     4.5 -    ID:         $Id$
     4.6      Author:     Florian Haftmann, TU Muenchen
     4.7  
     4.8  Introducing copies of types using trivial typedefs; datatype-like abstraction.
     4.9 @@ -75,7 +74,8 @@
    4.10  fun add_typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
    4.11    let
    4.12      val ty = Sign.certify_typ thy raw_ty;
    4.13 -    val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs;
    4.14 +    val vs =
    4.15 +      AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
    4.16      val tac = Tactic.rtac UNIV_witness 1;
    4.17      fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
    4.18        Rep_name = c_rep, Abs_inject = inject,
     5.1 --- a/src/Pure/Isar/expression.ML	Wed Dec 31 18:53:16 2008 +0100
     5.2 +++ b/src/Pure/Isar/expression.ML	Wed Dec 31 18:53:17 2008 +0100
     5.3 @@ -594,10 +594,11 @@
     5.4      val name = Sign.full_bname thy bname;
     5.5  
     5.6      val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
     5.7 -    val env = Term.add_term_free_names (body, []);
     5.8 +    val env = Term.add_free_names body [];
     5.9      val xs = filter (member (op =) env o #1) parms;
    5.10      val Ts = map #2 xs;
    5.11 -    val extraTs = (Term.term_tfrees body \\ fold Term.add_tfreesT Ts [])
    5.12 +    val extraTs =
    5.13 +      (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts [])
    5.14        |> Library.sort_wrt #1 |> map TFree;
    5.15      val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
    5.16  
     6.1 --- a/src/Pure/tctical.ML	Wed Dec 31 18:53:16 2008 +0100
     6.2 +++ b/src/Pure/tctical.ML	Wed Dec 31 18:53:17 2008 +0100
     6.3 @@ -485,9 +485,8 @@
     6.4    let
     6.5      fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
     6.6      fun find_vars thy (Const (c, ty)) =
     6.7 -        (case Term.typ_tvars ty
     6.8 -         of [] => I
     6.9 -          | _ => insert (op =) (c ^ typed ty))
    6.10 +          if null (Term.add_tvarsT ty []) then I
    6.11 +          else insert (op =) (c ^ typed ty)
    6.12        | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
    6.13        | find_vars _ (Free _) = I
    6.14        | find_vars _ (Bound _) = I
     7.1 --- a/src/Pure/thm.ML	Wed Dec 31 18:53:16 2008 +0100
     7.2 +++ b/src/Pure/thm.ML	Wed Dec 31 18:53:17 2008 +0100
     7.3 @@ -1154,7 +1154,7 @@
     7.4  (* Replace all TFrees not fixed or in the hyps by new TVars *)
     7.5  fun varifyT' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
     7.6    let
     7.7 -    val tfrees = List.foldr add_term_tfrees fixed hyps;
     7.8 +    val tfrees = fold Term.add_tfrees hyps fixed;
     7.9      val prop1 = attach_tpairs tpairs prop;
    7.10      val (al, prop2) = Type.varify tfrees prop1;
    7.11      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
     8.1 --- a/src/Tools/code/code_thingol.ML	Wed Dec 31 18:53:16 2008 +0100
     8.2 +++ b/src/Tools/code/code_thingol.ML	Wed Dec 31 18:53:17 2008 +0100
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      Tools/code/code_thingol.ML
     8.5 -    ID:         $Id$
     8.6      Author:     Florian Haftmann, TU Muenchen
     8.7  
     8.8  Intermediate language ("Thin-gol") representing executable code.
     8.9 @@ -620,7 +619,7 @@
    8.10      fun stmt_fun ((vs, raw_ty), raw_thms) =
    8.11        let
    8.12          val ty = Logic.unvarifyT raw_ty;
    8.13 -        val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
    8.14 +        val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
    8.15            then raw_thms
    8.16            else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
    8.17        in
     9.1 --- a/src/Tools/nbe.ML	Wed Dec 31 18:53:16 2008 +0100
     9.2 +++ b/src/Tools/nbe.ML	Wed Dec 31 18:53:17 2008 +0100
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      Tools/nbe.ML
     9.5 -    ID:         $Id$
     9.6      Authors:    Klaus Aehlig, LMU Muenchen; Tobias Nipkow, Florian Haftmann, TU Muenchen
     9.7  
     9.8  Normalization by evaluation, based on generic code generator.
     9.9 @@ -448,7 +447,7 @@
    9.10        singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
    9.11          (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
    9.12        (TypeInfer.constrain ty t);
    9.13 -    fun check_tvars t = if null (Term.term_tvars t) then t else
    9.14 +    fun check_tvars t = if null (Term.add_tvars t []) then t else
    9.15        error ("Illegal schematic type variables in normalized term: "
    9.16          ^ setmp show_types true (Syntax.string_of_term_global thy) t);
    9.17      val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);