1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Aug 26 09:23:21 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Aug 26 10:42:06 2010 +0200
     1.3 @@ -290,10 +290,12 @@
     1.4      | NONE => get_prover (default_atp_name ()))
     1.5    end
     1.6  
     1.7 +type locality = Sledgehammer_Fact_Filter.locality
     1.8 +
     1.9  local
    1.10  
    1.11  datatype sh_result =
    1.12 -  SH_OK of int * int * (string * bool) list |
    1.13 +  SH_OK of int * int * (string * locality) list |
    1.14    SH_FAIL of int * int |
    1.15    SH_ERROR
    1.16  
    1.17 @@ -355,8 +357,8 @@
    1.18      case result of
    1.19        SH_OK (time_isa, time_atp, names) =>
    1.20          let
    1.21 -          fun get_thms (name, chained) =
    1.22 -            ((name, chained), thms_of_name (Proof.context_of st) name)
    1.23 +          fun get_thms (name, loc) =
    1.24 +            ((name, loc), thms_of_name (Proof.context_of st) name)
    1.25          in
    1.26            change_data id inc_sh_success;
    1.27            change_data id (inc_sh_lemmas (length names));
    1.28 @@ -445,7 +447,7 @@
    1.29      then () else
    1.30      let
    1.31        val named_thms =
    1.32 -        Unsynchronized.ref (NONE : ((string * bool) * thm list) list option)
    1.33 +        Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
    1.34        val minimize = AList.defined (op =) args minimizeK
    1.35        val metis_ft = AList.defined (op =) args metis_ftK
    1.36