# HG changeset patch
# User wenzelm
# Date 1565256329 -7200
# Node ID c7ef6685c943010066b3ae5a66d2df32b3af4be2
# Parent  9cb269b49cf7be9cc1c52df49edb929e0527dfc0
clarified signature: fewer warnings in ML IDE;

diff -r 9cb269b49cf7 -r c7ef6685c943 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Aug 08 10:50:23 2019 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Aug 08 11:25:29 2019 +0200
@@ -144,8 +144,9 @@
 exception METIS_UNPROVABLE of unit
 
 (* Main function to start Metis proof and reconstruction *)
-fun FOL_SOLVE unused (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
+fun FOL_SOLVE unused type_encs lam_trans ctxt cls ths0 =
   let val thy = Proof_Context.theory_of ctxt
+      val type_enc :: fallback_type_encs = type_encs
       val new_skolem =
         Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy)
       val do_lams =