src/HOL/Inductive.thy
changeset 29281 b22ccb3998db
parent 29270 0eade173f77e
child 31604 eb2f9d709296
     1.1 --- a/src/HOL/Inductive.thy	Wed Dec 31 19:56:38 2008 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Wed Dec 31 20:31:36 2008 +0100
     1.3 @@ -362,7 +362,7 @@
     1.4  let
     1.5    fun fun_tr ctxt [cs] =
     1.6      let
     1.7 -      val x = Free (Name.variant (OldTerm.add_term_free_names (cs, [])) "x", dummyT);
     1.8 +      val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
     1.9        val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
    1.10                   ctxt [x, cs]
    1.11      in lambda x ft end