1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 25 23:02:50 2012 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jul 26 10:48:03 2012 +0200
     1.3 @@ -23,7 +23,6 @@
     1.4  val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
     1.5  val prover = hd provers
     1.6  *}
     1.7 -
     1.8  ML {*
     1.9  if do_it then
    1.10    generate_accessibility thy false "/tmp/mash_accessibility"
    1.11 @@ -47,7 +46,7 @@
    1.12  
    1.13  ML {*
    1.14  if do_it then
    1.15 -  generate_commands @{context} prover thy "/tmp/mash_commands"
    1.16 +  generate_commands @{context} params thy "/tmp/mash_commands"
    1.17  else
    1.18    ()
    1.19  *}

     2.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 25 23:02:50 2012 +0200
     2.2 +++ b/src/HOL/TPTP/mash_export.ML	Thu Jul 26 10:48:03 2012 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4      theory -> bool -> string -> unit
     2.5    val generate_atp_dependencies :
     2.6      Proof.context -> params -> theory -> bool -> string -> unit
     2.7 -  val generate_commands : Proof.context -> string -> theory -> string -> unit
     2.8 +  val generate_commands : Proof.context -> params -> theory -> string -> unit
     2.9    val generate_mepo_suggestions :
    2.10      Proof.context -> params -> theory -> int -> string -> unit
    2.11  end;
    2.12 @@ -51,6 +51,11 @@
    2.13  
    2.14  val all_names = map (rpair () o nickname_of) #> Symtab.make
    2.15  
    2.16 +fun smart_dependencies_of ctxt params prover facts all_names th =
    2.17 +  case atp_dependencies_of ctxt params prover 0 facts all_names th of
    2.18 +    SOME deps => deps
    2.19 +  | NONE => isar_dependencies_of all_names th |> these
    2.20 +
    2.21  fun generate_accessibility thy include_thy file_name =
    2.22    let
    2.23      val path = file_name |> Path.explode
    2.24 @@ -119,18 +124,16 @@
    2.25      fun do_thm th =
    2.26        let
    2.27          val name = nickname_of th
    2.28 -        val deps =
    2.29 -          case atp_dependencies_of ctxt params prover 0 facts all_names th of
    2.30 -            SOME deps => deps
    2.31 -          | NONE => isar_dependencies_of all_names th |> these
    2.32 +        val deps = smart_dependencies_of ctxt params prover facts all_names th
    2.33          val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
    2.34        in File.append path s end
    2.35    in List.app do_thm ths end
    2.36  
    2.37 -fun generate_commands ctxt prover thy file_name =
    2.38 +fun generate_commands ctxt (params as {provers, ...}) thy file_name =
    2.39    let
    2.40      val path = file_name |> Path.explode
    2.41      val _ = File.write path ""
    2.42 +    val prover = hd provers
    2.43      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    2.44      val facts = all_facts_of (Proof_Context.init_global thy) css_table
    2.45      val (new_facts, old_facts) =
    2.46 @@ -142,13 +145,13 @@
    2.47        let
    2.48          val name = nickname_of th
    2.49          val feats = features_of ctxt prover thy stature [prop_of th]
    2.50 -        val deps = isar_dependencies_of all_names th |> these
    2.51 +        val deps = smart_dependencies_of ctxt params prover facts all_names th
    2.52          val kind = Thm.legacy_get_kind th
    2.53 -        val core = escape_metas prevs ^ "; " ^ escape_metas feats
    2.54 +        val core =
    2.55 +          escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
    2.56 +          escape_metas feats
    2.57          val query = if kind <> "" then "? " ^ core ^ "\n" else ""
    2.58 -        val update =
    2.59 -          "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^
    2.60 -          escape_metas deps ^ "\n"
    2.61 +        val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
    2.62          val _ = File.append path (query ^ update)
    2.63        in [name] end
    2.64      val thy_map = old_facts |> thy_map_from_facts