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.
fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared;
authorblanchet
Tue, 20 Apr 2010 16:14:45 +0200
changeset 36237 86e62a98deea
parent 36236 5563c717638a
child 36238 344377ce2e0a
child 36263 56bf63d70120
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
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle