1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  signature SLEDGEHAMMER_MASH =
     1.6  sig
     1.7 -  type status = ATP_Problem_Generate.status
     1.8    type stature = ATP_Problem_Generate.stature
     1.9    type fact = Sledgehammer_Fact.fact
    1.10    type fact_override = Sledgehammer_Fact.fact_override
    1.11 @@ -33,7 +32,7 @@
    1.12    val theory_ord : theory * theory -> order
    1.13    val thm_ord : thm * thm -> order
    1.14    val features_of :
    1.15 -    Proof.context -> string -> theory -> status -> term list -> string list
    1.16 +    Proof.context -> string -> theory -> stature -> term list -> string list
    1.17    val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
    1.18    val goal_of_thm : theory -> thm -> thm
    1.19    val run_prover_for_mash :
    1.20 @@ -265,12 +264,13 @@
    1.21  val type_max_depth = 1
    1.22  
    1.23  (* TODO: Generate type classes for types? *)
    1.24 -fun features_of ctxt prover thy status ts =
    1.25 +fun features_of ctxt prover thy (scope, status) ts =
    1.26    thy_feature_name_of (Context.theory_name thy) ::
    1.27    interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
    1.28                                        ts
    1.29    |> forall is_lambda_free ts ? cons "no_lams"
    1.30    |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
    1.31 +  |> scope <> Global ? cons "local"
    1.32    |> (case status of
    1.33          General => I
    1.34        | Induction => cons "induction"
    1.35 @@ -525,7 +525,7 @@
    1.36      val thy = Proof_Context.theory_of ctxt
    1.37      val fact_graph = #fact_graph (mash_get ctxt)
    1.38      val parents = parents_wrt_facts facts fact_graph
    1.39 -    val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
    1.40 +    val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
    1.41      val suggs =
    1.42        if Graph.is_empty fact_graph then []
    1.43        else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
    1.44 @@ -568,7 +568,7 @@
    1.45              let
    1.46                val thy = Proof_Context.theory_of ctxt
    1.47                val name = timestamp () ^ " " ^ serial_string () (* freshish *)
    1.48 -              val feats = features_of ctxt prover thy General [t]
    1.49 +              val feats = features_of ctxt prover thy (Local, General) [t]
    1.50                val deps = used_ths |> map nickname_of
    1.51              in
    1.52                mash_map ctxt (fn {thys, fact_graph} =>
    1.53 @@ -613,11 +613,11 @@
    1.54                |> Symtab.make
    1.55          fun trim_deps deps = if length deps > max_dependencies then [] else deps
    1.56          fun do_fact _ (accum as (_, true)) = accum
    1.57 -          | do_fact ((_, (_, status)), th) ((parents, upds), false) =
    1.58 +          | do_fact ((_, stature), th) ((parents, upds), false) =
    1.59              let
    1.60                val name = nickname_of th
    1.61                val feats =
    1.62 -                features_of ctxt prover (theory_of_thm th) status [prop_of th]
    1.63 +                features_of ctxt prover (theory_of_thm th) stature [prop_of th]
    1.64                val deps = isabelle_dependencies_of all_names th |> trim_deps
    1.65                val upd = (name, parents, feats, deps)
    1.66              in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end