# HG changeset patch
# User wenzelm
# Date 1230745997 -3600
# Node ID fb3ccf499df5f4ca09e8b1ac00c983bcaf3d238b
# Parent  1d685baea08efea06a2966aa79c4a6abd5df07ed
use regular Term.add_XXX etc.;

diff -r 1d685baea08e -r fb3ccf499df5 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Wed Dec 31 18:53:17 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/recfun_codegen.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Code generator for recursive functions.
@@ -46,7 +45,7 @@
   | expand_eta thy (thms as thm :: _) =
       let
         val (_, ty) = Code_Unit.const_typ_eqn thm;
-      in if (null o Term.typ_tvars) ty orelse (null o fst o strip_type) ty
+      in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty
         then thms
         else map (Code_Unit.expand_eta thy 1) thms
       end;
diff -r 1d685baea08e -r fb3ccf499df5 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/HOL/Tools/refute.ML	Wed Dec 31 18:53:17 2008 +0100
@@ -790,7 +790,7 @@
       (* replace the (at most one) schematic type variable in each axiom *)
       (* by the actual type 'T'                                          *)
       val monomorphic_class_axioms = map (fn (axname, ax) =>
-        (case Term.term_tvars ax of
+        (case Term.add_tvars ax [] of
           [] =>
           (axname, ax)
         | [(idx, S)] =>
@@ -942,16 +942,13 @@
 (*               and all mutually recursive IDTs are considered.             *)
 (* ------------------------------------------------------------------------- *)
 
-  (* theory -> Term.term -> Term.typ list *)
-
   fun ground_types thy t =
   let
-    (* Term.typ * Term.typ list -> Term.typ list *)
-    fun collect_types (T, acc) =
+    fun collect_types T acc =
       (case T of
-        Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc))
+        Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
       | Type ("prop", [])      => acc
-      | Type ("set", [T1])     => collect_types (T1, acc)
+      | Type ("set", [T1])     => collect_types T1 acc
       | Type (s, Ts)           =>
         (case DatatypePackage.get_datatype thy s of
           SOME info =>  (* inductive datatype *)
@@ -976,9 +973,9 @@
             in
               case d of
                 DatatypeAux.DtTFree _ =>
-                collect_types (dT, acc)
+                collect_types dT acc
               | DatatypeAux.DtType (_, ds) =>
-                collect_types (dT, foldr collect_dtyp acc ds)
+                collect_types dT (foldr collect_dtyp acc ds)
               | DatatypeAux.DtRec i =>
                 if dT mem acc then
                   acc  (* prevent infinite recursion *)
@@ -1008,11 +1005,11 @@
         | NONE =>
           (* not an inductive datatype, e.g. defined via "typedef" or *)
           (* "typedecl"                                               *)
-          insert (op =) T (foldr collect_types acc Ts))
+          insert (op =) T (fold collect_types Ts acc))
       | TFree _                => insert (op =) T acc
       | TVar _                 => insert (op =) T acc)
   in
-    it_term_types collect_types (t, [])
+    fold_types collect_types t []
   end;
 
 (* ------------------------------------------------------------------------- *)
@@ -1287,7 +1284,7 @@
     (* terms containing them (their logical meaning is that there EXISTS a *)
     (* type s.t. ...; to refute such a formula, we would have to show that *)
     (* for ALL types, not ...)                                             *)
-    val _ = null (term_tvars t) orelse
+    val _ = null (Term.add_tvars t []) orelse
       error "Term to be refuted contains schematic type variables"
 
     (* existential closure over schematic variables *)
diff -r 1d685baea08e -r fb3ccf499df5 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed Dec 31 18:53:17 2008 +0100
@@ -405,7 +405,7 @@
 fun add_wanted_prfline ctxt ((lno, t, []), (nlines, lines)) =
       (nlines, (lno, t, []) :: lines)   (*conjecture clauses must be kept*)
   | add_wanted_prfline ctxt ((lno, t, deps), (nlines, lines)) =
-      if eq_types t orelse not (null (term_tvars t)) orelse
+      if eq_types t orelse not (null (Term.add_tvars t [])) orelse
          exists_subterm bad_free t orelse
          (not (null lines) andalso   (*final line can't be deleted for these reasons*)
           (length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0))   
diff -r 1d685baea08e -r fb3ccf499df5 src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/HOL/Tools/typecopy_package.ML	Wed Dec 31 18:53:17 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/typecopy_package.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Introducing copies of types using trivial typedefs; datatype-like abstraction.
@@ -75,7 +74,8 @@
 fun add_typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
   let
     val ty = Sign.certify_typ thy raw_ty;
-    val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs;
+    val vs =
+      AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
     val tac = Tactic.rtac UNIV_witness 1;
     fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
       Rep_name = c_rep, Abs_inject = inject,
diff -r 1d685baea08e -r fb3ccf499df5 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Dec 31 18:53:17 2008 +0100
@@ -594,10 +594,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 \\ fold Term.add_tfreesT 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;
 
diff -r 1d685baea08e -r fb3ccf499df5 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/Pure/tctical.ML	Wed Dec 31 18:53:17 2008 +0100
@@ -485,9 +485,8 @@
   let
     fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
     fun find_vars thy (Const (c, ty)) =
-        (case Term.typ_tvars ty
-         of [] => I
-          | _ => insert (op =) (c ^ typed ty))
+          if null (Term.add_tvarsT ty []) then I
+          else insert (op =) (c ^ typed ty)
       | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
       | find_vars _ (Free _) = I
       | find_vars _ (Bound _) = I
diff -r 1d685baea08e -r fb3ccf499df5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/Pure/thm.ML	Wed Dec 31 18:53:17 2008 +0100
@@ -1154,7 +1154,7 @@
 (* Replace all TFrees not fixed or in the hyps by new TVars *)
 fun varifyT' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
   let
-    val tfrees = List.foldr add_term_tfrees fixed hyps;
+    val tfrees = fold Term.add_tfrees hyps fixed;
     val prop1 = attach_tpairs tpairs prop;
     val (al, prop2) = Type.varify tfrees prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
diff -r 1d685baea08e -r fb3ccf499df5 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/Tools/code/code_thingol.ML	Wed Dec 31 18:53:17 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/code/code_thingol.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Intermediate language ("Thin-gol") representing executable code.
@@ -620,7 +619,7 @@
     fun stmt_fun ((vs, raw_ty), raw_thms) =
       let
         val ty = Logic.unvarifyT raw_ty;
-        val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
+        val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
           then raw_thms
           else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
       in
diff -r 1d685baea08e -r fb3ccf499df5 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Wed Dec 31 18:53:16 2008 +0100
+++ b/src/Tools/nbe.ML	Wed Dec 31 18:53:17 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/nbe.ML
-    ID:         $Id$
     Authors:    Klaus Aehlig, LMU Muenchen; Tobias Nipkow, Florian Haftmann, TU Muenchen
 
 Normalization by evaluation, based on generic code generator.
@@ -448,7 +447,7 @@
       singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
         (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
       (TypeInfer.constrain ty t);
-    fun check_tvars t = if null (Term.term_tvars t) then t else
+    fun check_tvars t = if null (Term.add_tvars t []) then t else
       error ("Illegal schematic type variables in normalized term: "
         ^ setmp show_types true (Syntax.string_of_term_global thy) t);
     val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);