src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML

    max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp,
    threshold_divisor = get args "threshold_divisor" threshold_divisor,
    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)
 val num_found_proofs = Unsynchronized.ref ([] : (int * int) list)
 val num_lost_proofs = Unsynchronized.ref ([] : (int * int) list)