tuned check_text;
authorwenzelm
Mon Sep 05 17:38:23 2005 +0200 (2005-09-05)
changeset 1726512d99bb4304b
parent 17264 c5b280a52a67
child 17266 31c23e8f8111
tuned check_text;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Sep 05 17:38:22 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Sep 05 17:38:23 2005 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4    val print_commands: Toplevel.transition -> Toplevel.transition
     1.5    val add_keywords: string list -> unit
     1.6    val add_parsers: parser list -> unit
     1.7 -  val check_text: string * Position.T -> bool -> Toplevel.state -> unit
     1.8 +  val check_text: string * Position.T -> Toplevel.state -> unit
     1.9    val deps_thy: string -> bool -> Path.T -> string list * Path.T list
    1.10    val load_thy: string -> bool -> bool -> Path.T -> unit
    1.11    val isar: bool -> bool -> unit Toplevel.isar
    1.12 @@ -234,8 +234,7 @@
    1.13  
    1.14  (* check_text *)
    1.15  
    1.16 -fun check_text s true state = (IsarOutput.eval_antiquote (#1 (get_lexicons ())) state s; ())
    1.17 -  | check_text _ false _ = ();
    1.18 +fun check_text s state = (IsarOutput.eval_antiquote (#1 (get_lexicons ())) state s; ());
    1.19  
    1.20  
    1.21  (* deps_thy *)