Nominal/Parser.thy
changeset 1685 721d92623c9d
parent 1683 f78c820f67c3
child 1744 00680cea0dde
equal deleted inserted replaced
1684:b9e4c812d2c6 1685:721d92623c9d
   592   in
   592   in
   593     map_index (prep_typ binds) annos
   593     map_index (prep_typ binds) annos
   594   end
   594   end
   595 
   595 
   596 in
   596 in
   597   map (map (map (map (fn (a, b, c) => (a, b, c, !alpha_type)))))
   597   map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type)))))
   598   (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
   598   (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
   599 end
   599 end
   600 *}
   600 *}
   601 
   601 
   602 ML {*
   602 ML {*