# HG changeset patch
# User wenzelm
# Date 1230678493 -3600
# Node ID 4a478f9d2847c891a452b36b543d4a8e9188d599
# Parent  5b4247055bd7132db922dcf4c75a2b1ab839556d
use regular Term.add_vars, Term.add_frees etc.;
moved old add_term_vars, add_term_frees etc. to structure OldTerm;

diff -r 5b4247055bd7 -r 4a478f9d2847 src/HOL/Tools/datatype_case.ML
--- a/src/HOL/Tools/datatype_case.ML	Wed Dec 31 00:08:13 2008 +0100
+++ b/src/HOL/Tools/datatype_case.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,7 +1,6 @@
 (*  Title:      HOL/Tools/datatype_case.ML
-    ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
-                Stefan Berghofer, TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
 
 Nested case expressions on datatypes.
 *)
@@ -426,9 +425,9 @@
 fun strip_case' dest (pat, rhs) =
   case dest (add_term_free_names (pat, [])) rhs of
     SOME (exp as Free _, clauses) =>
-      if member op aconv (term_frees pat) exp andalso
+      if member op aconv (OldTerm.term_frees pat) exp andalso
         not (exists (fn (_, rhs') =>
-          member op aconv (term_frees rhs') exp) clauses)
+          member op aconv (OldTerm.term_frees rhs') exp) clauses)
       then
         maps (strip_case' dest) (map (fn (pat', rhs') =>
           (subst_free [(exp, pat')] pat, rhs')) clauses)
@@ -451,7 +450,7 @@
     val thy = ProofContext.theory_of ctxt;
     val consts = ProofContext.consts_of ctxt;
     fun mk_clause (pat, rhs) =
-      let val xs = term_frees pat
+      let val xs = Term.add_frees pat []
       in
         Syntax.const "_case1" $
           map_aterms
@@ -459,8 +458,8 @@
               | Const (s, _) => Const (Consts.extern_early consts s, dummyT)
               | t => t) pat $
           map_aterms
-            (fn x as Free (s, _) =>
-                  if member op aconv xs x then Syntax.mark_bound s else x
+            (fn x as Free (s, T) =>
+                  if member (op =) xs (s, T) then Syntax.mark_bound s else x
               | t => t) rhs
       end
   in case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
diff -r 5b4247055bd7 -r 4a478f9d2847 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Wed Dec 31 00:08:13 2008 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -2,7 +2,7 @@
     Author:     Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory
     Copyright   Cambridge University 2007
 
-HOL setup for the Metis prover (version 2.0 from 2007).
+HOL setup for the Metis prover.
 *)
 
 signature METIS_TOOLS =
@@ -280,9 +280,10 @@
 
   fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
 
-  fun inst_excluded_middle th thy i_atm =
-    let val vx = hd (term_vars (prop_of th))
-        val substs = [(cterm_of thy vx, cterm_of thy i_atm)]
+  fun inst_excluded_middle thy i_atm =
+    let val th = EXCLUDED_MIDDLE
+        val [vx] = Term.add_vars (prop_of th) []
+        val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
     in  cterm_instantiate substs th  end;
 
   (* INFERENCE RULE: AXIOM *)
@@ -291,7 +292,7 @@
 
   (* INFERENCE RULE: ASSUME *)
   fun assume_inf ctxt atm =
-    inst_excluded_middle EXCLUDED_MIDDLE
+    inst_excluded_middle
       (ProofContext.theory_of ctxt)
       (singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm));
 
@@ -301,12 +302,12 @@
   fun inst_inf ctxt thpairs fsubst th =    
     let val thy = ProofContext.theory_of ctxt
         val i_th   = lookth thpairs th
-        val i_th_vars = term_vars (prop_of i_th)
-        fun find_var x = valOf (List.find (fn Term.Var((a,_),_) => a=x) i_th_vars)
+        val i_th_vars = Term.add_vars (prop_of i_th) []
+        fun find_var x = valOf (List.find (fn ((a,_),_) => a=x) i_th_vars)
         fun subst_translation (x,y) =
               let val v = find_var x
                   val t = fol_term_to_hol_RAW ctxt y (*we call infer_types below*)
-              in  SOME (cterm_of thy v, t)  end
+              in  SOME (cterm_of thy (Var v), t)  end
               handle Option =>
                   (Output.debug (fn() => "List.find failed for the variable " ^ x ^
                                          " in " ^ Display.string_of_thm i_th);
@@ -370,7 +371,7 @@
     end;
 
   (* INFERENCE RULE: REFL *)
-  val refl_x = cterm_of (the_context ()) (hd (term_vars (prop_of REFL_THM)));
+  val refl_x = cterm_of (the_context ()) (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   val refl_idx = 1 + Thm.maxidx_of REFL_THM;
 
   fun refl_inf ctxt t =
@@ -429,7 +430,7 @@
         val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
         val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm subst')
         val eq_terms = map (pairself (cterm_of thy))
-                           (ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
+                           (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
     in  cterm_instantiate eq_terms subst'  end;
 
   val factor = Seq.hd o distinct_subgoals_tac;
diff -r 5b4247055bd7 -r 4a478f9d2847 src/HOL/Tools/old_primrec_package.ML
--- a/src/HOL/Tools/old_primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Tools/old_primrec_package.ML
-    ID:         $Id$
-    Author:     Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
+    Author:     Norbert Voelker, FernUni Hagen
+    Author:     Stefan Berghofer, TU Muenchen
 
 Package for defining functions on datatypes by primitive recursion.
 *)
@@ -58,7 +58,7 @@
 fun process_eqn thy eq rec_fns =
   let
     val (lhs, rhs) =
-      if null (term_vars eq) then
+      if null (Term.add_vars eq []) then
         HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
         handle TERM _ => raise RecError "not a proper equation"
       else raise RecError "illegal schematic variable(s)";
@@ -91,7 +91,7 @@
     else
      (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
       check_vars "extra variables on rhs: "
-        (map dest_Free (term_frees rhs) \\ lfrees);
+        (map dest_Free (OldTerm.term_frees rhs) \\ lfrees);
       case AList.lookup (op =) rec_fns fnameT of
         NONE =>
           (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
diff -r 5b4247055bd7 -r 4a478f9d2847 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Dec 31 00:08:13 2008 +0100
+++ b/src/Pure/codegen.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/codegen.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Generic code generator.
@@ -598,7 +597,7 @@
      else Pretty.block (separate (Pretty.brk 1) (p :: ps));
 
 fun new_names t xs = Name.variant_list
-  (map (fst o fst o dest_Var) (term_vars t) union
+  (map (fst o fst o dest_Var) (OldTerm.term_vars t) union
     add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
 
 fun new_name t x = hd (new_names t [x]);
@@ -917,9 +916,9 @@
     val ctxt = ProofContext.init thy;
     val e =
       let
-        val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
+        val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
           error "Term to be evaluated contains type variables";
-        val _ = (null (term_vars t) andalso null (term_frees t)) orelse
+        val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
           error "Term to be evaluated contains variables";
         val (code, gr) = setmp mode ["term_of"]
           (generate_code_i thy [] "Generated")
diff -r 5b4247055bd7 -r 4a478f9d2847 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Dec 31 00:08:13 2008 +0100
+++ b/src/Tools/quickcheck.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -70,11 +70,11 @@
 
 fun prep_test_term t =
   let
-    val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
+    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
       error "Term to be tested contains type variables";
-    val _ = null (term_vars t) orelse
+    val _ = null (Term.add_vars t []) orelse
       error "Term to be tested contains schematic variables";
-    val frees = map dest_Free (term_frees t);
+    val frees = map dest_Free (OldTerm.term_frees t);
   in (map fst frees, list_abs_free (frees, t)) end
 
 fun test_term ctxt quiet generator_name size i t =
diff -r 5b4247055bd7 -r 4a478f9d2847 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,10 +1,9 @@
 (*  Title:      ZF/Tools/primrec_package.ML
-    ID:         $Id$
-    Author:     Stefan Berghofer and Norbert Voelker
-    Copyright   1998  TU Muenchen
-    ZF version by Lawrence C Paulson (Cambridge)
+    Author:     Norbert Voelker, FernUni Hagen
+    Author:     Stefan Berghofer, TU Muenchen
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
-Package for defining functions on datatypes by primitive recursion
+Package for defining functions on datatypes by primitive recursion.
 *)
 
 signature PRIMREC_PACKAGE =
@@ -33,7 +32,7 @@
 fun process_eqn thy (eq, rec_fn_opt) =
   let
     val (lhs, rhs) =
-        if null (term_vars eq) then
+        if null (Term.add_vars eq []) then
             dest_eqn eq handle TERM _ => raise RecError "not a proper equation"
         else raise RecError "illegal schematic variable(s)";
 
@@ -66,7 +65,7 @@
   in
     if has_duplicates (op =) lfrees then
       raise RecError "repeated variable name in pattern"
-    else if not ((map dest_Free (term_frees rhs)) subset lfrees) then
+    else if not ((map dest_Free (OldTerm.term_frees rhs)) subset lfrees) then
       raise RecError "extra variables on rhs"
     else if length middle > 1 then
       raise RecError "more than one non-variable in pattern"