# HG changeset patch
# User ballarin
# Date 1138871565 -3600
# Node ID 34a9e466201fe40b9cb1962d6145cd22e7dc4a3a
# Parent  da6e27ee69e5e58f2697436a8deb2a6266992838
*_asms_of fixed.

diff -r da6e27ee69e5 -r 34a9e466201f src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Feb 02 02:02:00 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Feb 02 10:12:45 2006 +0100
@@ -1270,10 +1270,11 @@
     val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
     val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
   in
-    elemss |> map (fn (_, es) => map (fn Int e => e) es)
+    elemss |> get
+      |> map (fn (_, es) => map (fn Int e => e) es)
       |> Library.flat
       |> Library.mapfilter (fn Assumes asms => SOME asms | _ => NONE)
-      |> get
+      |> Library.flat
       |> map (apsnd (map fst))
   end;
 
@@ -1284,10 +1285,10 @@
     |> map (fn ((p, T), mix) => (p, SOME T, mix));
 
 fun local_asms_of thy name =
-  gen_asms_of Library.last_elem thy name;
+  gen_asms_of (single o Library.last_elem) thy name;
 
 fun global_asms_of thy name =
-  gen_asms_of Library.flat thy name;
+  gen_asms_of I thy name;
 
 end (* local *)