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)