# HG changeset patch
# User blanchet
# Date 1272558292 -7200
# Node ID 061475351a09a35dc3deb2dba45f877e10cb868a
# Parent  96f767f546e7535003eaf10c7dbabb6eb1da1377
fix more "undeclared symbol" errors related to SPASS's DFG format

diff -r 96f767f546e7 -r 061475351a09 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 29 17:45:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 29 18:24:52 2010 +0200
@@ -358,19 +358,19 @@
 fun add_types tvars = fold add_fol_type_funcs tvars
 
 fun add_decls (full_types, explicit_apply, cma, cnh)
-              (CombConst ((c, _), _, tvars)) (funcs, preds) =
-      if c = "equal" then
-        (add_types tvars funcs, preds)
-      else
-        let val arity = min_arity_of cma c
-            val ntys = if not full_types then length tvars else 0
-            val addit = Symtab.update(c, arity+ntys)
-        in
-            if needs_hBOOL explicit_apply cnh c then
-              (add_types tvars (addit funcs), preds)
-            else
-              (add_types tvars funcs, addit preds)
-        end
+              (CombConst ((c, _), ctp, tvars)) (funcs, preds) =
+      (if c = "equal" then
+         (add_types tvars funcs, preds)
+       else
+         let val arity = min_arity_of cma c
+             val ntys = if not full_types then length tvars else 0
+             val addit = Symtab.update(c, arity + ntys)
+         in
+             if needs_hBOOL explicit_apply cnh c then
+               (add_types tvars (addit funcs), preds)
+             else
+               (add_types tvars funcs, addit preds)
+         end) |>> full_types ? add_fol_type_funcs ctp
   | add_decls _ (CombVar (_, ctp)) (funcs, preds) =
       (add_fol_type_funcs ctp funcs, preds)
   | add_decls params (CombApp (P, Q)) decls =