src/HOLCF/domain/syntax.ML
changeset 16394 495dbcd4f4c9
parent 16224 57094b83774e
child 16842 5979c46853d1
     1.1 --- a/src/HOLCF/domain/syntax.ML	Tue Jun 14 22:19:32 2005 +0200
     1.2 +++ b/src/HOLCF/domain/syntax.ML	Tue Jun 14 23:44:37 2005 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  open Domain_Library;
     1.5  infixr 5 -->; infixr 6 ->>;
     1.6  fun calc_syntax dtypeprod ((dname, typevars), 
     1.7 -	(cons': (string * mixfix * (bool*string*typ) list) list)) =
     1.8 +	(cons': (string * mixfix * (bool*string option*typ) list) list)) =
     1.9  let
    1.10  (* ----- constants concerning the isomorphism ------------------------------- *)
    1.11  
    1.12 @@ -49,7 +49,8 @@
    1.13  			   to generate parse rules for non-alphanumeric names*)
    1.14    fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_ssumT(oneT,mk_uT(mk_ctupleT(map third args))),
    1.15  			   Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
    1.16 -  fun sel (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ->> typ,NoSyn))args;
    1.17 +  fun sel1 (_,sel,typ)  = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
    1.18 +  fun sel (_   ,_,args) = List.mapPartial sel1 args;
    1.19  in
    1.20    val consts_con = map con cons';
    1.21    val consts_dis = map dis cons';
    1.22 @@ -100,7 +101,7 @@
    1.23  in (* local *)
    1.24  
    1.25  fun add_syntax (comp_dnam,eqs': ((string * typ list) *
    1.26 -	(string * mixfix * (bool*string*typ) list) list) list) thy'' =
    1.27 +	(string * mixfix * (bool*string option*typ) list) list) list) thy'' =
    1.28  let
    1.29    val dtypes  = map (Type o fst) eqs';
    1.30    val boolT   = HOLogic.boolT;