--- a/src/HOL/Inductive.thy Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Inductive.thy Thu Jun 09 16:34:49 2011 +0200
@@ -295,7 +295,8 @@
let
fun fun_tr ctxt [cs] =
let
- val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
+ (* FIXME proper name context!? *)
+ val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
in lambda x ft end
in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end