--- a/src/HOL/Inductive.thy Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Inductive.thy Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Inductive.thy
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
*)
@@ -363,7 +362,7 @@
let
fun fun_tr ctxt [cs] =
let
- val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT);
+ val x = Free (Name.variant (OldTerm.add_term_free_names (cs, [])) "x", dummyT);
val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
ctxt [x, cs]
in lambda x ft end