# HG changeset patch
# User wenzelm
# Date 1620814964 -7200
# Node ID a63d76ba0a03cc08c9c862792121e3523b00349f
# Parent  71c45d60a90a0d937243d7143a655d5bd24ad447
avoid duplicate loading of ML file;

diff -r 71c45d60a90a -r a63d76ba0a03 src/HOL/Mirabelle/Mirabelle.thy
--- a/src/HOL/Mirabelle/Mirabelle.thy	Wed May 12 06:35:16 2021 +0200
+++ b/src/HOL/Mirabelle/Mirabelle.thy	Wed May 12 12:22:44 2021 +0200
@@ -7,7 +7,6 @@
 begin
 
 ML_file \<open>Tools/mirabelle.ML\<close>
-ML_file \<open>../TPTP/sledgehammer_tactics.ML\<close>
 
 ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close>
 
diff -r 71c45d60a90a -r a63d76ba0a03 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Wed May 12 06:35:16 2021 +0200
+++ b/src/HOL/Sledgehammer.thy	Wed May 12 12:22:44 2021 +0200
@@ -33,5 +33,6 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
 
 end
diff -r 71c45d60a90a -r a63d76ba0a03 src/HOL/TPTP/ATP_Problem_Import.thy
--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Wed May 12 06:35:16 2021 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Wed May 12 12:22:44 2021 +0200
@@ -8,8 +8,6 @@
   imports Complex_Main TPTP_Interpret "HOL-Library.Refute"
 begin
 
-ML_file \<open>sledgehammer_tactics.ML\<close>
-
 ML \<open>Proofterm.proofs := 0\<close>
 
 declare [[show_consts]] (* for Refute *)
diff -r 71c45d60a90a -r a63d76ba0a03 src/HOL/TPTP/TPTP_Parser_Example.thy
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Wed May 12 06:35:16 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Wed May 12 12:22:44 2021 +0200
@@ -8,8 +8,6 @@
 imports TPTP_Parser TPTP_Interpret
 begin
 
-ML_file "sledgehammer_tactics.ML"
-
 import_tptp "$TPTP/Problems/LCL/LCL414+1.p"
 
 ML \<open>
diff -r 71c45d60a90a -r a63d76ba0a03 src/HOL/TPTP/sledgehammer_tactics.ML
--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed May 12 06:35:16 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-(*  Title:      HOL/TPTP/sledgehammer_tactics.ML
-    Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2010, 2011
-
-Sledgehammer as a tactic.
-*)
-
-signature SLEDGEHAMMER_TACTICS =
-sig
-  type fact_override = Sledgehammer_Fact.fact_override
-
-  val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override ->
-    thm list -> int -> tactic
-  val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override ->
-    thm list -> int -> tactic
-end;
-
-structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_Fact
-open Sledgehammer_Prover
-open Sledgehammer_Prover_ATP
-open Sledgehammer_Prover_Minimize
-open Sledgehammer_MaSh
-open Sledgehammer_Commands
-
-fun run_prover override_params fact_override chained i n ctxt goal =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val mode = Normal
-    val params as {provers, max_facts, ...} = default_params thy override_params
-    val name = hd provers
-    val prover = get_prover ctxt mode name
-    val default_max_facts = default_max_facts_of_prover ctxt name
-    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
-    val ho_atp = exists (is_ho_atp ctxt) provers
-    val keywords = Thy_Header.get_keywords' ctxt
-    val css_table = clasimpset_rule_table_of ctxt
-    val facts =
-      nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t
-      |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override
-        hyp_ts concl_t
-      |> hd |> snd
-    val problem =
-      {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
-       factss = [("", facts)], found_proof = I}
-  in
-    (case prover params problem of
-      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
-    | _ => NONE)
-    handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
-  end
-
-fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th =
-  let val override_params = override_params @ [("preplay_timeout", "0")] in
-    (case run_prover override_params fact_override chained i i ctxt th of
-      SOME facts =>
-      Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
-        (maps (thms_of_name ctxt) facts) i th
-    | NONE => Seq.empty)
-  end
-
-fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th =
-  let
-    val override_params =
-      override_params @
-      [("preplay_timeout", "0"),
-       ("minimize", "false")]
-    val xs = run_prover override_params fact_override chained i i ctxt th
-  in
-    if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty
-  end
-
-end;
diff -r 71c45d60a90a -r a63d76ba0a03 src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Wed May 12 12:22:44 2021 +0200
@@ -0,0 +1,76 @@
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_tactics.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2010, 2011
+
+Sledgehammer as a tactic.
+*)
+
+signature SLEDGEHAMMER_TACTICS =
+sig
+  type fact_override = Sledgehammer_Fact.fact_override
+
+  val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override ->
+    thm list -> int -> tactic
+  val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override ->
+    thm list -> int -> tactic
+end;
+
+structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Fact
+open Sledgehammer_Prover
+open Sledgehammer_Prover_ATP
+open Sledgehammer_Prover_Minimize
+open Sledgehammer_MaSh
+open Sledgehammer_Commands
+
+fun run_prover override_params fact_override chained i n ctxt goal =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val mode = Normal
+    val params as {provers, max_facts, ...} = default_params thy override_params
+    val name = hd provers
+    val prover = get_prover ctxt mode name
+    val default_max_facts = default_max_facts_of_prover ctxt name
+    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
+    val ho_atp = exists (is_ho_atp ctxt) provers
+    val keywords = Thy_Header.get_keywords' ctxt
+    val css_table = clasimpset_rule_table_of ctxt
+    val facts =
+      nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t
+      |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override
+        hyp_ts concl_t
+      |> hd |> snd
+    val problem =
+      {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
+       factss = [("", facts)], found_proof = I}
+  in
+    (case prover params problem of
+      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
+    | _ => NONE)
+    handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
+  end
+
+fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th =
+  let val override_params = override_params @ [("preplay_timeout", "0")] in
+    (case run_prover override_params fact_override chained i i ctxt th of
+      SOME facts =>
+      Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
+        (maps (thms_of_name ctxt) facts) i th
+    | NONE => Seq.empty)
+  end
+
+fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th =
+  let
+    val override_params =
+      override_params @
+      [("preplay_timeout", "0"),
+       ("minimize", "false")]
+    val xs = run_prover override_params fact_override chained i i ctxt th
+  in
+    if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty
+  end
+
+end;