do not choke on type variables emerging during rewriting
authorhaftmann
Fri Jun 28 21:07:32 2013 +0200 (2013-06-28)
changeset 52473a2407f62a29f
parent 52472 3a43a8b1ecb0
child 52474 9c7f760d06c2
do not choke on type variables emerging during rewriting
src/Tools/nbe.ML
     1.1 --- a/src/Tools/nbe.ML	Fri Jun 28 14:51:19 2013 +0200
     1.2 +++ b/src/Tools/nbe.ML	Fri Jun 28 21:07:32 2013 +0200
     1.3 @@ -133,12 +133,13 @@
     1.4      val algebra = Sign.classes_of thy;
     1.5      val triv_classes = get_triv_classes thy;
     1.6      val vs = Term.add_tfrees t [];
     1.7 -  in t
     1.8 +  in
     1.9 +    t
    1.10      |> (map_types o map_type_tfree)
    1.11          (fn (v, sort) => TFree (v, Sorts.inter_sort algebra (sort, triv_classes)))
    1.12      |> rew
    1.13      |> (map_types o map_type_tfree)
    1.14 -        (fn (v, _) => TFree (v, the (AList.lookup (op =) vs v)))
    1.15 +        (fn (v, sort) => TFree (v, the_default sort (AList.lookup (op =) vs v)))
    1.16    end;
    1.17  
    1.18  end;