--- a/src/HOL/TPTP/mash_export.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/TPTP/mash_export.ML Wed Mar 04 19:53:18 2015 +0100
@@ -58,7 +58,7 @@
| _ => ("", []))
fun has_thm_thy th thy =
- Context.theory_name thy = Context.theory_name (theory_of_thm th)
+ Context.theory_name thy = Context.theory_name (Thm.theory_of_thm th)
fun has_thys thys th = exists (has_thm_thy th) thys
@@ -98,7 +98,7 @@
fun do_fact ((_, stature), th) =
let
val name = nickname_of_thm th
- val feats = features_of ctxt (theory_of_thm th) stature [prop_of th]
+ val feats = features_of ctxt (Thm.theory_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 (theory_of_thm th) stature [prop_of th]
+ val goal_feats = features_of ctxt (Thm.theory_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) =
- [prop_of th]
- |> features_of ctxt (theory_of_thm th) stature
+ [Thm.prop_of th]
+ |> features_of ctxt (Thm.theory_of_thm th) stature
|> map (rpair (weight * extra_feature_factor))
val query =
@@ -261,7 +261,7 @@
val suggs =
old_facts
|> filter_accessible_from th
- |> mepo_or_mash_suggested_facts ctxt (theory_of_thm th) params max_suggs hyp_ts
+ |> mepo_or_mash_suggested_facts ctxt (Thm.theory_of_thm th) params max_suggs hyp_ts
concl_t
|> map (nickname_of_thm o snd)
in