--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/datatype_rep_proofs.ML
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Definitional introduction of datatypes
@@ -8,7 +7,6 @@
- injectivity of constructors
- distinctness of constructors
- induction theorem
-
*)
signature DATATYPE_REP_PROOFS =
@@ -85,7 +83,7 @@
val branchT = if null branchTs then HOLogic.unitT
else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
val arities = get_arities descr' \ 0;
- val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
+ val unneeded_vars = hd tyvars \\ foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
val recTs = get_rec_types descr' sorts;
val newTs = Library.take (length (hd descr), recTs);
@@ -369,7 +367,7 @@
val prop = Thm.prop_of thm;
val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
(_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
- val used = add_term_tfree_names (a, []);
+ val used = OldTerm.add_term_tfree_names (a, []);
fun mk_thm i =
let