--- 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 =
--- 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