Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
eta-expand to make SML/NJ happy
authorblanchet
Wed, 25 May 2011 08:31:36 +0200
changeset 42975 284f9a7af1c9
parent 42974 347d5197896e
child 42976 9901f877eeb7
eta-expand to make SML/NJ happy
src/HOL/Tools/ATP/atp_proof.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle