src/HOL/Tools/ATP/atp_proof.ML
changeset 43816 284f9a7af1c9
parent 43814 6b39a2098ffd
child 43839 1c80902d0456
     1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 18:04:23 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed May 25 08:31:36 2011 +0200
     1.3 @@ -511,7 +511,7 @@
     1.4                            deps) ::
     1.5      clean_up_dependencies (name :: seen) steps
     1.6  
     1.7 -val clean_up_atp_proof_dependencies = clean_up_dependencies []
     1.8 +fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
     1.9  
    1.10  fun map_term_names_in_term f (ATerm (s, ts)) =
    1.11    ATerm (f s, map (map_term_names_in_term f) ts)