1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Apr 20 16:04:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Apr 20 16:14:45 2010 +0200
     1.3 @@ -377,8 +377,9 @@
     1.4      handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
     1.5  
     1.6  fun decls_of_clauses params clauses arity_clauses =
     1.7 -  let val functab = init_functab |> Symtab.update (type_wrapper, 2)
     1.8 -                                 |> Symtab.update ("hAPP", 2)
     1.9 +  let val functab =
    1.10 +        init_functab |> fold Symtab.update [(type_wrapper, 2), ("hAPP", 2),
    1.11 +                                            ("tc_bool", 0)]
    1.12        val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
    1.13        val (functab, predtab) =
    1.14          (functab, predtab) |> fold (add_clause_decls params) clauses