made SML/NJ happy;
authorwenzelm
Wed Dec 29 12:16:49 2010 +0100 (2010-12-29)
changeset 414072878845bc549
parent 41406 062490d081b9
child 41408 08a072ca6348
made SML/NJ happy;
more accurate dependencies;
src/HOL/IsaMakefile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Dec 28 18:28:52 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Dec 29 12:16:49 2010 +0100
     1.3 @@ -1314,6 +1314,7 @@
     1.4    Mirabelle/Tools/mirabelle_quickcheck.ML				\
     1.5    Mirabelle/Tools/mirabelle_refute.ML					\
     1.6    Mirabelle/Tools/mirabelle_sledgehammer.ML 				\
     1.7 +  Mirabelle/Tools/mirabelle_sledgehammer_filter.ML			\
     1.8    Mirabelle/Tools/sledgehammer_tactics.ML
     1.9  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
    1.10  
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Dec 28 18:28:52 2010 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Dec 29 12:16:49 2010 +0100
     2.3 @@ -39,9 +39,9 @@
     2.4     ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold}
     2.5  
     2.6  structure Prooftab =
     2.7 -  Table(type key = int * int val ord = prod_ord int_ord int_ord);
     2.8 +  Table(type key = int * int val ord = prod_ord int_ord int_ord)
     2.9  
    2.10 -val proof_table = Unsynchronized.ref Prooftab.empty
    2.11 +val proof_table = Unsynchronized.ref (Prooftab.empty: string list list Prooftab.table)
    2.12  
    2.13  val num_successes = Unsynchronized.ref ([] : (int * int) list)
    2.14  val num_failures = Unsynchronized.ref ([] : (int * int) list)