# HG changeset patch
# User ballarin
# Date 1228856439 -3600
# Node ID 3ad4cf50070dc993caac437fac06eb437badea13
# Parent  e74341997a487d7d9f559ad797a8d0a4fcb979b8
Correct order of defines in specification.

diff -r e74341997a48 -r 3ad4cf50070d src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Dec 09 21:27:00 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Dec 09 22:00:39 2008 +0100
@@ -774,7 +774,7 @@
 
     val loc_ctxt = thy' |>
       NewLocale.register_locale bname (extraTs, params)
-        (asm, defs) ([], [])
+        (asm, rev defs) ([], [])
         (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
       NewLocale.init name;