diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/Parser.thy --- a/Nominal/Parser.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal/Parser.thy Mon Apr 26 10:01:13 2010 +0200 @@ -625,9 +625,14 @@ map_index (prep_typ binds) annos end + val result = 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))) + + val _ = warning (@{make_string} result) + in - 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))) + result end *}