# HG changeset patch
# User wenzelm
# Date 1125934703 -7200
# Node ID 12d99bb4304ba471ca6e9a2e73628669b26dd65c
# Parent  c5b280a52a6726f99f1dd2a5664f20a9b578db7e
tuned check_text;

diff -r c5b280a52a67 -r 12d99bb4304b src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Sep 05 17:38:22 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Sep 05 17:38:23 2005 +0200
@@ -34,7 +34,7 @@
   val print_commands: Toplevel.transition -> Toplevel.transition
   val add_keywords: string list -> unit
   val add_parsers: parser list -> unit
-  val check_text: string * Position.T -> bool -> Toplevel.state -> unit
+  val check_text: string * Position.T -> Toplevel.state -> unit
   val deps_thy: string -> bool -> Path.T -> string list * Path.T list
   val load_thy: string -> bool -> bool -> Path.T -> unit
   val isar: bool -> bool -> unit Toplevel.isar
@@ -234,8 +234,7 @@
 
 (* check_text *)
 
-fun check_text s true state = (IsarOutput.eval_antiquote (#1 (get_lexicons ())) state s; ())
-  | check_text _ false _ = ();
+fun check_text s state = (IsarOutput.eval_antiquote (#1 (get_lexicons ())) state s; ());
 
 
 (* deps_thy *)