src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
changeset 70586 57df8a85317a
parent 63692 1bc4bc2c9fd1
child 72401 2783779b7dd3
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Aug 20 11:01:05 2019 +0200
@@ -38,7 +38,7 @@
   val string_of_proof_method : Proof.context -> string list -> proof_method -> string
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
   val string_of_play_outcome : play_outcome -> string
-  val play_outcome_ord : play_outcome * play_outcome -> order
+  val play_outcome_ord : play_outcome ord
   val one_line_proof_text : Proof.context -> int -> one_line_params -> string
 end;