# HG changeset patch
# User desharna
# Date 1695994572 -7200
# Node ID 70e1c0167ae26503b07d5fcfff67229b7a88d31e
# Parent  fc179b4423b4578f1454cb22b595eef11537529f
removed unused function parameter

diff -r fc179b4423b4 -r 70e1c0167ae2 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Sep 29 14:00:09 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Sep 29 15:36:12 2023 +0200
@@ -377,7 +377,7 @@
    ("slice", "false"),
    ("timeout", timeout |> Time.toSeconds |> string_of_int)]
 
-fun run_proof_method trivial full name meth named_thms timeout pos st =
+fun run_proof_method trivial name meth named_thms timeout pos st =
   let
     fun do_method named_thms ctxt =
       let
@@ -400,9 +400,6 @@
           ORELSE' SMT_Solver.smt_tac ctxt thms
         else if meth = "smt" then
           SMT_Solver.smt_tac ctxt thms
-        else if full then
-          Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN]
-            ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
         else if String.isPrefix "metis (" meth then
           let
             val (type_encs, lam_trans) =
@@ -477,7 +474,7 @@
             val (log2, change_data2) =
               (case proof_method_and_used_thms of
                 SOME (proof_method, used_thms) =>
-                run_proof_method trivial false name proof_method used_thms timeout pos pre
+                run_proof_method trivial name proof_method used_thms timeout pos pre
                 |> apfst (prefix (proof_method ^ " (sledgehammer): "))
               | NONE => ("", I))
             val () = Synchronized.change data