# HG changeset patch
# User wenzelm
# Date 895054741 -7200
# Node ID f66f67577cf316476e0104729cf3d3dbfb5d9fc5
# Parent  7c22890a7a9b1b231cdc6cb13da3c9a6a7277e24
gen_attr: fixed order of evaluation;

diff -r 7c22890a7a9b -r f66f67577cf3 src/Pure/attribute.ML
--- a/src/Pure/attribute.ML	Wed May 13 12:17:49 1998 +0200
+++ b/src/Pure/attribute.ML	Wed May 13 12:19:01 1998 +0200
@@ -149,15 +149,16 @@
 
 (* get global / local attributes *)
 
-fun gen_attr which thy (raw_name, args) =
+fun gen_attr which thy =
   let
     val {space, attrs} = get_attributes thy;
-    val name = NameSpace.intern space raw_name;
-  in
-    (case Symtab.lookup (attrs, name) of
-      None => raise FAIL (name, "unknown attribute")
-    | Some p => which p args)
-  end;
+    val intern = NameSpace.intern space;
+
+    fun attr (raw_name, args) x_th =
+      (case Symtab.lookup (attrs, intern raw_name) of
+        None => raise FAIL (intern raw_name, "unknown attribute")
+      | Some p => which p args x_th);
+  in attr end;
 
 val global_attr = gen_attr fst;
 val local_attr = gen_attr snd;