# HG changeset patch
# User wenzelm
# Date 1222884157 -7200
# Node ID 0586b855c2b5217e7da183bdd2559fe54266874e
# Parent  504c4edead134221d6d22d3722f35dd6169c1ad7
datatype transition: internal trans field is maintained in reverse order;
tuned;

diff -r 504c4edead13 -r 0586b855c2b5 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Oct 01 18:16:14 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Oct 01 20:02:37 2008 +0200
@@ -385,9 +385,9 @@
 
 fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
   | apply_union int pos (tr :: trs) state =
-      apply_tr int pos tr state
-        handle UNDEF => apply_union int pos trs state
-          | FAILURE (alt_state, UNDEF) => apply_union int pos trs alt_state
+      apply_union int pos trs state
+        handle UNDEF => apply_tr int pos tr state
+          | FAILURE (alt_state, UNDEF) => apply_tr int pos tr alt_state
           | exn as FAILURE _ => raise exn
           | exn => raise FAILURE (state, exn);
 
@@ -437,8 +437,8 @@
 
 (* modify transitions *)
 
-fun name nm = map_transition (fn (_, pos, int_only, print, no_timing, trans) =>
-  (nm, pos, int_only, print, no_timing, trans));
+fun name name = map_transition (fn (_, pos, int_only, print, no_timing, trans) =>
+  (name, pos, int_only, print, no_timing, trans));
 
 fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) =>
   (name, pos, int_only, print, no_timing, trans));
@@ -450,7 +450,7 @@
   (name, pos, int_only, print, true, trans));
 
 fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) =>
-  (name, pos, int_only, print, no_timing, trans @ [tr]));
+  (name, pos, int_only, print, no_timing, tr :: trans));
 
 val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, _) =>
   (name, pos, int_only, print, no_timing, []));