--- a/src/CCL/Wfd.thy Wed Dec 31 00:01:51 2008 +0100
+++ b/src/CCL/Wfd.thy Wed Dec 31 00:08:11 2008 +0100
@@ -1,5 +1,4 @@
(* Title: CCL/Wfd.thy
- ID: $Id$
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
@@ -451,7 +450,7 @@
fun is_rigid_prog t =
case (Logic.strip_assums_concl t) of
- (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => (term_vars a = [])
+ (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => null (Term.add_vars a [])
| _ => false
in
--- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Dec 31 00:01:51 2008 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Dec 31 00:08:11 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/datatype_abs_proofs.ML
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Proofs and defintions independent of concrete representation
@@ -10,8 +9,7 @@
- characteristic equations for primrec combinators
- characteristic equations for case combinators
- equations for splitting "P (case ...)" expressions
- - "nchotomy" and "case_cong" theorems for TFL
-
+ - "nchotomy" and "case_cong" theorems for TFL
*)
signature DATATYPE_ABS_PROOFS =
@@ -425,8 +423,8 @@
val (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ Ma)) = tm;
val cert = cterm_of thy;
val nchotomy' = nchotomy RS spec;
- val nchotomy'' = cterm_instantiate
- [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
+ val [v] = Term.add_vars (concl_of nchotomy') [];
+ val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy'
in
SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {prems, ...} =>
--- a/src/HOL/Tools/typedef_package.ML Wed Dec 31 00:01:51 2008 +0100
+++ b/src/HOL/Tools/typedef_package.ML Wed Dec 31 00:08:11 2008 +0100
@@ -176,7 +176,7 @@
fun show_names pairs = commas_quote (map fst pairs);
val illegal_vars =
- if null (term_vars set) andalso null (term_tvars set) then []
+ if null (Term.add_vars set []) andalso null (Term.add_tvars set []) then []
else ["Illegal schematic variable(s) on rhs"];
val dup_lhs_tfrees =
@@ -188,8 +188,8 @@
| extras => ["Extra type variables on rhs: " ^ show_names extras]);
val illegal_frees =
- (case term_frees set of [] => []
- | xs => ["Illegal variables on rhs: " ^ show_names (map dest_Free xs)]);
+ (case Term.add_frees set [] of [] => []
+ | xs => ["Illegal variables on rhs: " ^ show_names xs]);
val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
val _ = if null errs then () else error (cat_lines errs);
--- a/src/Pure/tctical.ML Wed Dec 31 00:01:51 2008 +0100
+++ b/src/Pure/tctical.ML Wed Dec 31 00:08:11 2008 +0100
@@ -1,7 +1,5 @@
(* Title: Pure/tctical.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
Tacticals.
*)
@@ -404,19 +402,18 @@
(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
Instantiates distinct free variables by terms of same type.*)
fun free_instantiate ctpairs =
- forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
+ forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
- fun free_of s ((a,i), T) =
- Free(s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i),
- T)
+ fun free_of s ((a, i), T) =
+ Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T)
- fun mk_inst (var as Var(v,T)) = (var, free_of "METAHYP1_" (v,T))
+ fun mk_inst v = (Var v, free_of "METAHYP1_" v)
in
(*Common code for METAHYPS and metahyps_thms*)
fun metahyps_split_prem prem =
let (*find all vars in the hyps -- should find tvars also!*)
- val hyps_vars = List.foldr add_term_vars [] (Logic.strip_assums_hyp prem)
+ val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) []
val insts = map mk_inst hyps_vars
(*replace the hyps_vars by Frees*)
val prem' = subst_atomic insts prem
@@ -434,20 +431,18 @@
val cparams = map cterm fparams
fun swap_ctpair (t,u) = (cterm u, cterm t)
(*Subgoal variables: make Free; lift type over params*)
- fun mk_subgoal_inst concl_vars (var as Var(v,T)) =
- if member (op =) concl_vars var
- then (var, true, free_of "METAHYP2_" (v,T))
- else (var, false,
- free_of "METAHYP2_" (v, map #2 params --->T))
+ fun mk_subgoal_inst concl_vars (v, T) =
+ if member (op =) concl_vars (v, T)
+ then ((v, T), true, free_of "METAHYP2_" (v, T))
+ else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
(*Instantiate subgoal vars by Free applied to params*)
- fun mk_ctpair (t,in_concl,u) =
- if in_concl then (cterm t, cterm u)
- else (cterm t, cterm (list_comb (u,fparams)))
+ fun mk_ctpair (v, in_concl, u) =
+ if in_concl then (cterm (Var v), cterm u)
+ else (cterm (Var v), cterm (list_comb (u, fparams)))
(*Restore Vars with higher type and index*)
- fun mk_subgoal_swap_ctpair
- (t as Var((a,i),_), in_concl, u as Free(_,U)) =
- if in_concl then (cterm u, cterm t)
- else (cterm u, cterm(Var((a, i+maxidx), U)))
+ fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
+ if in_concl then (cterm u, cterm (Var ((a, i), T)))
+ else (cterm u, cterm (Var ((a, i + maxidx), U)))
(*Embed B in the original context of params and hyps*)
fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
(*Strip the context using elimination rules*)
@@ -456,8 +451,8 @@
fun relift st =
let val prop = Thm.prop_of st
val subgoal_vars = (*Vars introduced in the subgoals*)
- List.foldr add_term_vars [] (Logic.strip_imp_prems prop)
- and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
+ fold Term.add_vars (Logic.strip_imp_prems prop) []
+ and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
val emBs = map (cterm o embed) (prems_of st')
--- a/src/Tools/code/code_ml.ML Wed Dec 31 00:01:51 2008 +0100
+++ b/src/Tools/code/code_ml.ML Wed Dec 31 00:08:11 2008 +0100
@@ -954,7 +954,7 @@
fun eval eval'' term_of reff thy ct args =
let
val ctxt = ProofContext.init thy;
- val _ = if null (term_frees (term_of ct)) then () else error ("Term "
+ val _ = if null (Term.add_frees (term_of ct) []) then () else error ("Term "
^ quote (Syntax.string_of_term_global thy (term_of ct))
^ " to be evaluated contains free variables");
fun eval' naming program ((vs, ty), t) deps =