--- 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)