# HG changeset patch
# User wenzelm
# Date 1230678491 -3600
# Node ID 4ea3358fac3fa3691562973984f5bd8f6cac1c91
# Parent  bf99ccf71b7c2be1af91710d40f0f10c59d99322
use regular Term.add_vars, Term.add_frees etc.;

diff -r bf99ccf71b7c -r 4ea3358fac3f src/CCL/Wfd.thy
--- 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
 
diff -r bf99ccf71b7c -r 4ea3358fac3f src/HOL/Tools/datatype_abs_proofs.ML
--- 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, ...} => 
diff -r bf99ccf71b7c -r 4ea3358fac3f src/HOL/Tools/typedef_package.ML
--- 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);
diff -r bf99ccf71b7c -r 4ea3358fac3f src/Pure/tctical.ML
--- 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')
diff -r bf99ccf71b7c -r 4ea3358fac3f src/Tools/code/code_ml.ML
--- 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 =