# HG changeset patch
# User wenzelm
# Date 1465557537 -7200
# Node ID 4f3402f35be7ecea33886364f872097350e73da8
# Parent  302daf91896687367ebf5725284857ba2ac8ece6
tuned;

diff -r 302daf918966 -r 4f3402f35be7 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Jun 10 12:45:34 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jun 10 13:18:57 2016 +0200
@@ -27,7 +27,7 @@
   val parse_spans: Token.T list -> Command_Span.span list
   val side_comments: Token.T list -> Token.T list
   val command_reports: theory -> Token.T -> Position.report_text list
-  val check_command: Proof.context -> string * Position.T -> string
+  val check_command: Proof.context -> command_keyword -> string
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =