--- a/src/HOL/IsaMakefile Tue Dec 28 18:28:52 2010 +0100
+++ b/src/HOL/IsaMakefile Wed Dec 29 12:16:49 2010 +0100
@@ -1314,6 +1314,7 @@
Mirabelle/Tools/mirabelle_quickcheck.ML \
Mirabelle/Tools/mirabelle_refute.ML \
Mirabelle/Tools/mirabelle_sledgehammer.ML \
+ Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \
Mirabelle/Tools/sledgehammer_tactics.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Dec 28 18:28:52 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Dec 29 12:16:49 2010 +0100
@@ -39,9 +39,9 @@
ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold}
structure Prooftab =
- Table(type key = int * int val ord = prod_ord int_ord int_ord);
+ Table(type key = int * int val ord = prod_ord int_ord int_ord)
-val proof_table = Unsynchronized.ref Prooftab.empty
+val proof_table = Unsynchronized.ref (Prooftab.empty: string list list Prooftab.table)
val num_successes = Unsynchronized.ref ([] : (int * int) list)
val num_failures = Unsynchronized.ref ([] : (int * int) list)