diff -r 42202671777c -r dbac573b27e7 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Feb 01 18:45:18 2016 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Feb 01 19:57:58 2016 +0100
@@ -17,7 +17,7 @@
     thm list * thm Seq.seq
   val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic
   val metis_method : (string list option * string option) * thm list -> Proof.context -> thm list ->
-    thm -> thm Seq.seq
+    tactic
   val metis_lam_transs : string list
   val parse_metis_options : (string list option * string option) parser
 end