src/HOL/Inductive.thy
changeset 43324 2b47822868e4
parent 41081 fb1e5377143d
child 43580 023a1d1f97bd
     1.1 --- a/src/HOL/Inductive.thy	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -295,7 +295,8 @@
     1.4  let
     1.5    fun fun_tr ctxt [cs] =
     1.6      let
     1.7 -      val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
     1.8 +      (* FIXME proper name context!? *)
     1.9 +      val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
    1.10        val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
    1.11      in lambda x ft end
    1.12  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end