tuned;

--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Tue Jun 05 18:36:09 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Tue Jun 05 18:36:10 2007 +0200
@@ -40,12 +40,10 @@
 
 structure Data = GenericDataFun
 (
-  val name = "HOL/norm";
   type T = (thm * entry) list;
   val empty = [];
   val extend = I;
   fun merge _ = AList.merge eq_key (K true);
-  fun print _ _ = ();
 );
 
 val get = Data.get o Context.Proof;

--- a/src/HOL/Tools/function_package/fundef_lib.ML	Tue Jun 05 18:36:09 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Tue Jun 05 18:36:10 2007 +0200
@@ -99,11 +99,12 @@
   | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
 
 
-(* term.ML *)
+(* 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)