# HG changeset patch
# User krauss
# Date 1230930416 -3600
# Node ID e02b3a32f34f22135257094427a4e0c346a153f1
# Parent  b074c05f00ad8287e659bdcf4b4765d4f377a37f
removed references to OldTerm.*

diff -r b074c05f00ad -r e02b3a32f34f src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Fri Jan 02 16:21:47 2009 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML	Fri Jan 02 22:06:56 2009 +0100
@@ -80,7 +80,7 @@
     let 
       val t' = snd (dest_all_all t)
       val (assumes, concl) = Logic.strip_horn t'
-    in (fold (curry OldTerm.add_term_vars) assumes [], OldTerm.term_vars concl)
+    in (fold Term.add_vars assumes [], Term.add_vars concl [])
     end
 
 fun cong_deps crule =
@@ -89,7 +89,9 @@
     in
       IntGraph.empty
         |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
-        |> fold_product (fn (i,(c1,_)) => fn (j,(_, t2)) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
+        |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) => 
+               if i = j orelse null (c1 inter t2) 
+               then I else IntGraph.add_edge_acyclic (i,j))
              num_branches num_branches
     end
     
diff -r b074c05f00ad -r e02b3a32f34f src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Fri Jan 02 16:21:47 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Fri Jan 02 22:06:56 2009 +0100
@@ -436,7 +436,7 @@
                                   |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
                                   |> forall_intr (cterm_of thy x)
                                   |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
-                                  |> (fn it => fold (forall_intr o cterm_of thy) (OldTerm.term_vars (prop_of it)) it)
+                                  |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
 
         val goalstate =  Conjunction.intr graph_is_function complete
                           |> Thm.close_derivation
diff -r b074c05f00ad -r e02b3a32f34f src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Jan 02 16:21:47 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Jan 02 22:06:56 2009 +0100
@@ -63,9 +63,10 @@
 
 fun inst_case_thm thy x P thm =
     let
-        val [Pv, xv] = OldTerm.term_vars (prop_of thm)
+        val [Pv, xv] = Term.add_vars (prop_of thm) []
     in
-        cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
+        cterm_instantiate [(cterm_of thy (Var xv), cterm_of thy x), 
+                           (cterm_of thy (Var Pv), cterm_of thy P)] thm
     end