# HG changeset patch
# User wenzelm
# Date 1221937541 -7200
# Node ID e2f0913918653b46c35c57a614ebf7f96cd0a643
# Parent  5097b8c0f59f86672d2ab8ccc523945a73836e36
made SML/NJ happy;

diff -r 5097b8c0f59f -r e2f091391865 src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Fri Sep 19 22:11:50 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Sat Sep 20 21:05:41 2008 +0200
@@ -233,9 +233,7 @@
 
 (* interactive state transformations *)
 
-local nonfix >> >>> in
-
-fun >> raw_tr =
+fun op >> raw_tr =
   let
     val id = create_command raw_tr;
     val {category, transition = tr, ...} = the_command id;
@@ -254,10 +252,8 @@
         true))
   end;
 
-fun >>> [] = ()
-  | >>> (tr :: trs) = if >> tr then >>> trs else ();
-
-end;
+fun op >>> [] = ()
+  | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
 
 
 (* implicit navigation wrt. proper commands *)
@@ -316,7 +312,7 @@
   in
     (case Source.get_single (Source.set_prompt (prompt_markup Source.default_prompt) src) of
       NONE => if secure then quit () else ()
-    | SOME (tr, src') => if >> tr orelse check_secure () then raw_loop secure src' else ())
+    | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
     handle exn => (Output.error_msg (Toplevel.exn_message exn) handle crash =>
       (CRITICAL (fn () => change crashes (cons crash));
         warning "Recovering after Isar toplevel crash -- see also Isar.crashes");