changeset 54284 | 0b53378080d9 |
parent 54283 | 6f0a49ed1bb1 |
child 54286 | 22616f65d4ea |
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Nov 06 22:42:54 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Nov 06 22:50:12 2013 +0100 @@ -339,7 +339,6 @@ if exists (exists_subtype_in seen) mutual_Ts then (case gen_rhss_in gen_seen rho mutual_Ts of [] => fresh_tyargs () - | [gen_tyargs] => (rho, gen_tyargs, gen_seen, lthy) | gen_tyargss as gen_tyargs :: gen_tyargss_tl => let val unify_pairs = split_list (maps (curry (op ~~) gen_tyargs) gen_tyargss_tl);