# HG changeset patch
# User ballarin
# Date 1255637203 -7200
# Node ID d556a0e04e33eb5cf1b8b9cf201ce9036a4bad23
# Parent  484863ae9b98e1cfc63d99b9680507adf13e77f5
Observe order of declaration when printing registrations.

diff -r 484863ae9b98 -r d556a0e04e33 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Oct 01 23:03:59 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Oct 15 22:06:43 2009 +0200
@@ -427,7 +427,7 @@
   in
     (case these_registrations thy name of
         [] => Pretty.str ("no interpretations")
-      | regs => Pretty.big_list "interpretations:" (map prt_reg regs))
+      | regs => Pretty.big_list "interpretations:" (map prt_reg (rev regs)))
     |> Pretty.writeln
   end;