src/HOL/Inductive.thy
changeset 29270 0eade173f77e
parent 26793 e36a92ff543e
child 29281 b22ccb3998db
     1.1 --- a/src/HOL/Inductive.thy	Wed Dec 31 15:30:10 2008 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Wed Dec 31 18:53:16 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Inductive.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Markus Wenzel, TU Muenchen
     1.7  *)
     1.8  
     1.9 @@ -363,7 +362,7 @@
    1.10  let
    1.11    fun fun_tr ctxt [cs] =
    1.12      let
    1.13 -      val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT);
    1.14 +      val x = Free (Name.variant (OldTerm.add_term_free_names (cs, [])) "x", dummyT);
    1.15        val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
    1.16                   ctxt [x, cs]
    1.17      in lambda x ft end