# HG changeset patch
# User blanchet
# Date 1306305096 -7200
# Node ID 284f9a7af1c946d1c17e1eb482c4de087f394026
# Parent  347d5197896ea876d40ed0ad538f94f77f1caf0f
eta-expand to make SML/NJ happy

diff -r 347d5197896e -r 284f9a7af1c9 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 18:04:23 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed May 25 08:31:36 2011 +0200
@@ -511,7 +511,7 @@
                           deps) ::
     clean_up_dependencies (name :: seen) steps
 
-val clean_up_atp_proof_dependencies = clean_up_dependencies []
+fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
 
 fun map_term_names_in_term f (ATerm (s, ts)) =
   ATerm (f s, map (map_term_names_in_term f) ts)