--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 20 16:17:34 2005 +0200
@@ -79,7 +79,7 @@
else fold_bal (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 leafTs = leafTs' @ (map (fn n => TFree (n, valOf (assoc (sorts, n)))) unneeded_vars);
+ 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);
val oldTs = Library.drop (length (hd descr), recTs);