# HG changeset patch
# User blanchet
# Date 1383774612 -3600
# Node ID 0b53378080d94240799e945a5fccdb68f51dcc5b
# Parent  6f0a49ed1bb139c7f78dc34c9b18f9b9f6dfeb08
simplified code

diff -r 6f0a49ed1bb1 -r 0b53378080d9 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- 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);