src/HOL/Tools/datatype_rep_proofs.ML
changeset 17521 0f1c48de39f5
parent 17412 e26cb20ef0cc
child 17959 8db36a108213
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -79,7 +79,7 @@
     1.4        else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
     1.5      val arities = get_arities descr' \ 0;
     1.6      val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
     1.7 -    val leafTs = leafTs' @ (map (fn n => TFree (n, valOf (assoc (sorts, n)))) unneeded_vars);
     1.8 +    val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
     1.9      val recTs = get_rec_types descr' sorts;
    1.10      val newTs = Library.take (length (hd descr), recTs);
    1.11      val oldTs = Library.drop (length (hd descr), recTs);