# HG changeset patch
# User blanchet
# Date 1271772885 -7200
# Node ID 86e62a98deea8ac14bd1a5ce1e78506ec891ecdf
# Parent  5563c717638aec144e0d148a1f6ed30370dd8c68
fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared;
this bug occurs when the explicit "hAPP" or "hBOOL" functions are introduced and full types is activated

diff -r 5563c717638a -r 86e62a98deea src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Apr 20 16:04:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Apr 20 16:14:45 2010 +0200
@@ -377,8 +377,9 @@
     handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
 
 fun decls_of_clauses params clauses arity_clauses =
-  let val functab = init_functab |> Symtab.update (type_wrapper, 2)
-                                 |> Symtab.update ("hAPP", 2)
+  let val functab =
+        init_functab |> fold Symtab.update [(type_wrapper, 2), ("hAPP", 2),
+                                            ("tc_bool", 0)]
       val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
       val (functab, predtab) =
         (functab, predtab) |> fold (add_clause_decls params) clauses