1.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -81,11 +81,11 @@
     1.4      val facts =
     1.5        all_facts_of thy css_table
     1.6        |> not include_thy ? filter_out (has_thy thy o snd)
     1.7 -    fun do_fact ((_, (_, status)), th) =
     1.8 +    fun do_fact ((_, stature), th) =
     1.9        let
    1.10          val name = nickname_of th
    1.11          val feats =
    1.12 -          features_of ctxt prover (theory_of_thm th) status [prop_of th]
    1.13 +          features_of ctxt prover (theory_of_thm th) stature [prop_of th]
    1.14          val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n"
    1.15        in File.append path s end
    1.16    in List.app do_fact facts end
    1.17 @@ -165,10 +165,10 @@
    1.18              |>> sort (thm_ord o pairself snd)
    1.19      val ths = facts |> map snd
    1.20      val all_names = all_names ths
    1.21 -    fun do_fact ((_, (_, status)), th) prevs =
    1.22 +    fun do_fact ((_, stature), th) prevs =
    1.23        let
    1.24          val name = nickname_of th
    1.25 -        val feats = features_of ctxt prover thy status [prop_of th]
    1.26 +        val feats = features_of ctxt prover thy stature [prop_of th]
    1.27          val deps = isabelle_dependencies_of all_names th
    1.28          val kind = Thm.legacy_get_kind th
    1.29          val core = escape_metas prevs ^ "; " ^ escape_metas feats

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     2.3 @@ -6,7 +6,6 @@
     2.4  
     2.5  signature SLEDGEHAMMER_MASH =
     2.6  sig
     2.7 -  type status = ATP_Problem_Generate.status
     2.8    type stature = ATP_Problem_Generate.stature
     2.9    type fact = Sledgehammer_Fact.fact
    2.10    type fact_override = Sledgehammer_Fact.fact_override
    2.11 @@ -33,7 +32,7 @@
    2.12    val theory_ord : theory * theory -> order
    2.13    val thm_ord : thm * thm -> order
    2.14    val features_of :
    2.15 -    Proof.context -> string -> theory -> status -> term list -> string list
    2.16 +    Proof.context -> string -> theory -> stature -> term list -> string list
    2.17    val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
    2.18    val goal_of_thm : theory -> thm -> thm
    2.19    val run_prover_for_mash :
    2.20 @@ -265,12 +264,13 @@
    2.21  val type_max_depth = 1
    2.22  
    2.23  (* TODO: Generate type classes for types? *)
    2.24 -fun features_of ctxt prover thy status ts =
    2.25 +fun features_of ctxt prover thy (scope, status) ts =
    2.26    thy_feature_name_of (Context.theory_name thy) ::
    2.27    interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
    2.28                                        ts
    2.29    |> forall is_lambda_free ts ? cons "no_lams"
    2.30    |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
    2.31 +  |> scope <> Global ? cons "local"
    2.32    |> (case status of
    2.33          General => I
    2.34        | Induction => cons "induction"
    2.35 @@ -525,7 +525,7 @@
    2.36      val thy = Proof_Context.theory_of ctxt
    2.37      val fact_graph = #fact_graph (mash_get ctxt)
    2.38      val parents = parents_wrt_facts facts fact_graph
    2.39 -    val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
    2.40 +    val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
    2.41      val suggs =
    2.42        if Graph.is_empty fact_graph then []
    2.43        else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
    2.44 @@ -568,7 +568,7 @@
    2.45              let
    2.46                val thy = Proof_Context.theory_of ctxt
    2.47                val name = timestamp () ^ " " ^ serial_string () (* freshish *)
    2.48 -              val feats = features_of ctxt prover thy General [t]
    2.49 +              val feats = features_of ctxt prover thy (Local, General) [t]
    2.50                val deps = used_ths |> map nickname_of
    2.51              in
    2.52                mash_map ctxt (fn {thys, fact_graph} =>
    2.53 @@ -613,11 +613,11 @@
    2.54                |> Symtab.make
    2.55          fun trim_deps deps = if length deps > max_dependencies then [] else deps
    2.56          fun do_fact _ (accum as (_, true)) = accum
    2.57 -          | do_fact ((_, (_, status)), th) ((parents, upds), false) =
    2.58 +          | do_fact ((_, stature), th) ((parents, upds), false) =
    2.59              let
    2.60                val name = nickname_of th
    2.61                val feats =
    2.62 -                features_of ctxt prover (theory_of_thm th) status [prop_of th]
    2.63 +                features_of ctxt prover (theory_of_thm th) stature [prop_of th]
    2.64                val deps = isabelle_dependencies_of all_names th |> trim_deps
    2.65                val upd = (name, parents, feats, deps)
    2.66              in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end