src/HOL/Inductive.thy

 (*  Title:      HOL/Inductive.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
 header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *}
 

 
 parse_translation (advanced) {*
 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
 in [("_lam_pats_syntax", fun_tr)] end
 *}