--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 01 23:52:06 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