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.
hopefully this will help the SML/NJ type inference
authorblanchet
Thu, 05 May 2011 10:24:12 +0200
changeset 42694 30278eb9c9db
parent 42693 3c2baf9b3c61
child 42695 a94ad372b2f5
hopefully this will help the SML/NJ type inference
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 10:16:14 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 10:24:12 2011 +0200
@@ -887,7 +887,7 @@
       case type_sys of
         Preds (Polymorphic, All_Types) => insert_type #3 decl decls
       | _ => insert (op =) decl decls
-    fun do_term tm =
+    and do_term tm =
       let val (head, args) = strip_combterm_comb tm in
         (case head of
            CombConst ((s, s'), T, T_args) =>
isabelle