src/HOL/Tools/datatype_package.ML

 (*  Title:      HOL/Tools/datatype_package.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Datatype package for Isabelle/HOL.
 *)
 

     fun no_constr (c, T) = error ("Bad constructor: "
       ^ Sign.extern_const thy c ^ "::"
       ^ Syntax.string_of_typ_global thy T);
     fun type_of_constr (cT as (_, T)) =
       let
-        val frees = typ_tfrees T;
+        val frees = OldTerm.typ_tfrees T;
         val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
           handle TYPE _ => no_constr cT
         val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
         val _ = if length frees <> length vs then no_constr cT else ();
       in (tyco, (vs, cT)) end;

     fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) =
       let
         fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
           let
             val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
-            val _ = (case fold (curry add_typ_tfree_names) cargs' [] \\ tvs of
+            val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
                 [] => ()
               | vs => error ("Extra type variables on rhs: " ^ commas vs))
           in (constrs @ [((if flat_names then Sign.full_bname tmp_thy else
                 Sign.full_bname_path tmp_thy tname) (Syntax.const_name cname mx'),
                    map (dtyp_of_typ new_dts) cargs')],