# HG changeset patch
# User wenzelm
# Date 1435927903 -7200
# Node ID 58326c4a3ea2f355a539649430924ff0872611e4
# Parent  6686a410842a464c91720580a2d0363e91b04004
tuned signature;

diff -r 6686a410842a -r 58326c4a3ea2 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Jul 03 14:41:55 2015 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 03 14:51:43 2015 +0200
@@ -98,7 +98,7 @@
     fun do_fact ((_, stature), th) =
       let
         val name = nickname_of_thm th
-        val feats = features_of ctxt (Thm.theory_of_thm th) stature [Thm.prop_of th]
+        val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
         val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
       in
         File.append path s
@@ -188,14 +188,14 @@
           val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
           val isar_deps = isar_dependencies_of name_tabs th
           val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps)
-          val goal_feats = features_of ctxt (Thm.theory_of_thm th) stature [Thm.prop_of th]
+          val goal_feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
           val access_facts = filter_accessible_from th new_facts @ old_facts
           val (marker, deps) =
             smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps
 
           fun extra_features_of (((_, stature), th), weight) =
             [Thm.prop_of th]
-            |> features_of ctxt (Thm.theory_of_thm th) stature
+            |> features_of ctxt (Thm.theory_name_of_thm th) stature
             |> map (rpair (weight * extra_feature_factor))
 
           val query =
diff -r 6686a410842a -r 58326c4a3ea2 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 03 14:41:55 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 03 14:51:43 2015 +0200
@@ -52,7 +52,7 @@
   val goal_of_thm : theory -> thm -> thm
   val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm ->
     prover_result
-  val features_of : Proof.context -> theory -> stature -> term list -> string list
+  val features_of : Proof.context -> string -> stature -> term list -> string list
   val trim_dependencies : string list -> string list option
   val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option
   val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
@@ -922,12 +922,10 @@
 val type_max_depth = 1
 
 (* TODO: Generate type classes for types? *)
-fun features_of ctxt thy (scope, _) ts =
-  let val thy_name = Context.theory_name thy in
-    thy_feature_of thy_name ::
-    term_features_of ctxt thy_name term_max_depth type_max_depth ts
-    |> scope <> Global ? cons local_feature
-  end
+fun features_of ctxt thy_name (scope, _) ts =
+  thy_feature_of thy_name ::
+  term_features_of ctxt thy_name term_max_depth type_max_depth ts
+  |> scope <> Global ? cons local_feature
 
 (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn
    from such proofs. *)
@@ -1160,13 +1158,14 @@
 
     fun chained_or_extra_features_of factor (((_, stature), th), weight) =
       [Thm.prop_of th]
-      |> features_of ctxt (Thm.theory_of_thm th) stature
+      |> features_of ctxt (Thm.theory_name_of_thm th) stature
       |> map (rpair (weight * factor))
 
     val {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} =
       peek_state ctxt
 
-    val goal_feats0 = features_of ctxt thy (Local, General) (concl_t :: hyp_ts)
+    val goal_feats0 =
+      features_of ctxt (Context.theory_name thy) (Local, General) (concl_t :: hyp_ts)
     val chained_feats = chained
       |> map (rpair 1.0)
       |> map (chained_or_extra_features_of chained_feature_factor)
@@ -1263,7 +1262,7 @@
     launch_thread timeout (fn () =>
       let
         val thy = Proof_Context.theory_of ctxt
-        val feats = features_of ctxt thy (Local, General) [t]
+        val feats = features_of ctxt (Context.theory_name thy) (Local, General) [t]
         val facts = rev_sort_list_prefix (crude_thm_ord o apply2 snd) 1 facts
       in
         map_state ctxt
@@ -1373,7 +1372,7 @@
               (learns, (num_nontrivial, next_commit, _)) =
             let
               val name = nickname_of_thm th
-              val feats = features_of ctxt (Thm.theory_of_thm th) stature [Thm.prop_of th]
+              val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
               val deps = these (deps_of status th)
               val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
               val learns = (name, parents, feats, deps) :: learns