src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42694 30278eb9c9db
parent 42693 3c2baf9b3c61
child 42697 9bc5dc48f1a5
--- 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) =>