--- a/src/HOL/Tools/Datatype/datatype.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Aug 10 20:53:43 2011 +0200
@@ -77,7 +77,7 @@
else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
val unneeded_vars =
- subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
+ subtract (op =) (List.foldr Misc_Legacy.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val (newTs, oldTs) = chop (length (hd descr)) recTs;
@@ -372,7 +372,7 @@
val prop = Thm.prop_of thm;
val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
(_ $ (_ $ (r $ (a $ _)) $ _)) = Type.legacy_freeze prop;
- val used = OldTerm.add_term_tfree_names (a, []);
+ val used = Misc_Legacy.add_term_tfree_names (a, []);
fun mk_thm i =
let
@@ -676,7 +676,7 @@
let
val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
val _ =
- (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
+ (case subtract (op =) tvs (fold (curry Misc_Legacy.add_typ_tfree_names) cargs' []) of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs));
val c = Sign.full_name_path tmp_thy tname' cname;