Nominal/Fv.thy
changeset 1911 60b5c61d3de2
parent 1896 996d4411e95e
equal deleted inserted replaced
1910:57891245370d 1911:60b5c61d3de2
   135      Otherwise we return: argl = argr
   135      Otherwise we return: argl = argr
   136 
   136 
   137 *)
   137 *)
   138 
   138 
   139 ML {*
   139 ML {*
   140 datatype alpha_type = AlphaGen | AlphaRes | AlphaLst;
   140 datatype alpha_mode = AlphaGen | AlphaRes | AlphaLst;
   141 *}
   141 *}
   142 
   142 
   143 ML {*
   143 ML {*
   144 fun atyp_const AlphaGen = @{const_name alpha_gen}
   144 fun atyp_const AlphaGen = @{const_name alpha_gen}
   145   | atyp_const AlphaRes = @{const_name alpha_res}
   145   | atyp_const AlphaRes = @{const_name alpha_res}