src/HOLCF/domain/syntax.ML
changeset 3534 c245c88194ff
parent 2453 2d416226b27d
child 3771 ede66fb99880
     1.1 --- a/src/HOLCF/domain/syntax.ML	Fri Jul 18 13:54:41 1997 +0200
     1.2 +++ b/src/HOLCF/domain/syntax.ML	Fri Jul 18 13:55:09 1997 +0200
     1.3 @@ -79,13 +79,15 @@
     1.4  	fun arg1 n (con,_,args) = if args = [] then expvar n 
     1.5  				  else mk_appl (Constant "LAM ") 
     1.6  		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
     1.7 -  in mk_appl (Constant "@case") [Variable "x", foldr'
     1.8 +  in
     1.9 +    ParsePrintRule
    1.10 +      (mk_appl (Constant "@case") [Variable "x", foldr'
    1.11  				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
    1.12 -				 (mapn case1 1 cons')] <->
    1.13 -     mk_appl (Constant "@fapp") [foldl 
    1.14 +				 (mapn case1 1 cons')],
    1.15 +       mk_appl (Constant "@fapp") [foldl 
    1.16  				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
    1.17  				 (Constant (dname^"_when"),mapn arg1 1 cons'),
    1.18 -				 Variable "x"]
    1.19 +				 Variable "x"])
    1.20    end;
    1.21  end;
    1.22