--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Jan 01 21:23:32 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Thu Jan 02 09:50:22 2014 +0100
@@ -336,7 +336,7 @@
if exists (exists_subtype_in seen) mutual_Ts then
(case gen_rhss_in gen_seen rho mutual_Ts of
[] => fresh_tyargs ()
- | gen_tyargss as gen_tyargs :: gen_tyargss_tl =>
+ | gen_tyargs :: gen_tyargss_tl =>
let
val unify_pairs = split_list (maps (curry (op ~~) gen_tyargs) gen_tyargss_tl);
val mgu = Type.raw_unifys unify_pairs Vartab.empty;