# HG changeset patch
# User wenzelm
# Date 1293621409 -3600
# Node ID 2878845bc549ceef616d6856e0cb4448663a6884
# Parent  062490d081b9d5ef637b3c6daefc12c2dfdbd426
made SML/NJ happy;
more accurate dependencies;

diff -r 062490d081b9 -r 2878845bc549 src/HOL/IsaMakefile
--- 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
 
diff -r 062490d081b9 -r 2878845bc549 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- 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)