gen_attr: fixed order of evaluation;
authorwenzelm
Wed, 13 May 1998 12:19:01 +0200
changeset 4918 f66f67577cf3
parent 4917 7c22890a7a9b
child 4919 9397b1446cdb
gen_attr: fixed order of evaluation;
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;