made SML/NJ happy;
authorwenzelm
Mon Aug 08 13:39:51 2011 +0200 (2011-08-08)
changeset 440533cc902f81a26
parent 44052 00f0c8782a51
child 44054 da5fcc0f6c52
made SML/NJ happy;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Aug 08 13:29:54 2011 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Aug 08 13:39:51 2011 +0200
     1.3 @@ -274,14 +274,14 @@
     1.4  
     1.5  fun case_names cs =
     1.6    Rule_Cases.case_names (map fst cs) #>
     1.7 -  Rule_Cases.cases_hyp_names (map (map hname o snd) cs)
     1.8 +  Rule_Cases.cases_hyp_names (map (map hname o snd) cs);
     1.9  
    1.10  val hnamesP =
    1.11    Scan.optional
    1.12 -    (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]")
    1.13 -    []
    1.14 +    (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") [];
    1.15  
    1.16 -val case_namesP = Scan.lift (Scan.repeat1 (Args.name -- hnamesP))
    1.17 +fun case_namesP x = Scan.lift (Scan.repeat1 (Args.name -- hnamesP)) x;
    1.18 +
    1.19  
    1.20  (* misc rules *)
    1.21