Nominal/Parser.thy
changeset 1685 721d92623c9d
parent 1683 f78c820f67c3
child 1744 00680cea0dde
--- a/Nominal/Parser.thy	Sat Mar 27 16:17:45 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 27 16:20:39 2010 +0100
@@ -594,7 +594,7 @@
   end
 
 in
-  map (map (map (map (fn (a, b, c) => (a, b, c, !alpha_type)))))
+  map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type)))))
   (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
 end
 *}