# HG changeset patch
# User krauss
# Date 1218202600 -7200
# Node ID e4a4d057749d3d76e4c1a44f9dc2a8734f2f4e2f
# Parent  23d2567c578e9022d33c5acce40032e5bcbd22c3
clean up dead code

diff -r 23d2567c578e -r e4a4d057749d src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Fri Aug 08 13:36:44 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Fri Aug 08 15:36:40 2008 +0200
@@ -94,17 +94,7 @@
   | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
 
 
-(* FIXME cf. Term.exists_subterm *)
-fun forall_aterms P (t $ u) = forall_aterms P t andalso forall_aterms P u
-  | forall_aterms P (Abs (_, _, t)) = forall_aterms P t
-  | forall_aterms P a = P a
-
-(* FIXME cf. Term.exists_subterm *)
-fun exists_aterm P = not o forall_aterms (not o P)
-
-
-
-(* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *)
+(* Replaces Frees by name. Works with loose Bounds. *)
 fun replace_frees assoc =
     map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
                  | t => t)
@@ -116,14 +106,12 @@
 fun mk_forall_rename (n, v) =
     rename_bound n o Logic.all v 
 
-val dummy_term = Free ("", dummyT)
-
 fun forall_intr_rename (n, cv) thm =
     let
       val allthm = forall_intr cv thm
       val (_ $ abs) = prop_of allthm
     in
-      Thm.rename_boundvars abs (Abs (n, dummyT, dummy_term)) allthm
+      Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
     end