# HG changeset patch
# User wenzelm
# Date 1217862814 -7200
# Node ID c8a462f1f4a2b3626da16a51b76127c956bcdc85
# Parent  de34a576c7568e3ede42f5bf26d0f1029310495f
simplified prepare_command;

diff -r de34a576c756 -r c8a462f1f4a2 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 04 17:13:33 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Aug 04 17:13:34 2008 +0200
@@ -24,7 +24,7 @@
   val print_outer_syntax: unit -> unit
   val scan: string -> OuterLex.token list
   val parse: Position.T -> string -> Toplevel.transition list
-  val prepare_command: Markup.property list -> string * Position.T -> Toplevel.transition
+  val prepare_command: Position.T -> string -> Toplevel.transition
   val process_file: Path.T -> theory -> theory
   type isar
   val isar: bool -> isar
@@ -196,12 +196,10 @@
   |> toplevel_source false NONE get_parser
   |> Source.exhaust;
 
-fun prepare_command props (str, pos) =
-  let val pos' = Position.of_properties (props |> Position.default_properties pos) in
-    (case parse pos' str of
-      [transition] => transition
-    | _ => error "exactly one command expected")
-  end;
+fun prepare_command pos str =
+  (case parse pos str of
+    [transition] => transition
+  | _ => error "exactly one command expected");
 
 
 (* process file *)