# HG changeset patch
# User wenzelm
# Date 1312803591 -7200
# Node ID 3cc902f81a26a4f4775500291afea1dbd881293e
# Parent  00f0c8782a51d4e7cf6825cbf4c7787de64c0548
made SML/NJ happy;

diff -r 00f0c8782a51 -r 3cc902f81a26 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Aug 08 13:29:54 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Aug 08 13:39:51 2011 +0200
@@ -274,14 +274,14 @@
 
 fun case_names cs =
   Rule_Cases.case_names (map fst cs) #>
-  Rule_Cases.cases_hyp_names (map (map hname o snd) cs)
+  Rule_Cases.cases_hyp_names (map (map hname o snd) cs);
 
 val hnamesP =
   Scan.optional
-    (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]")
-    []
+    (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") [];
 
-val case_namesP = Scan.lift (Scan.repeat1 (Args.name -- hnamesP))
+fun case_namesP x = Scan.lift (Scan.repeat1 (Args.name -- hnamesP)) x;
+
 
 (* misc rules *)