--- 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;
--- 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 *)
--- 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))
--- 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,
--- 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;
--- 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
--- 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);
--- 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
--- 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);