# HG changeset patch
# User haftmann
# Date 1372446452 -7200
# Node ID a2407f62a29fe77fc3ae2b99a218ab24463710df
# Parent  3a43a8b1ecb0212f80af1c479b880d34b89b09d4
do not choke on type variables emerging during rewriting

diff -r 3a43a8b1ecb0 -r a2407f62a29f src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Fri Jun 28 14:51:19 2013 +0200
+++ b/src/Tools/nbe.ML	Fri Jun 28 21:07:32 2013 +0200
@@ -133,12 +133,13 @@
     val algebra = Sign.classes_of thy;
     val triv_classes = get_triv_classes thy;
     val vs = Term.add_tfrees t [];
-  in t
+  in
+    t
     |> (map_types o map_type_tfree)
         (fn (v, sort) => TFree (v, Sorts.inter_sort algebra (sort, triv_classes)))
     |> rew
     |> (map_types o map_type_tfree)
-        (fn (v, _) => TFree (v, the (AList.lookup (op =) vs v)))
+        (fn (v, sort) => TFree (v, the_default sort (AList.lookup (op =) vs v)))
   end;
 
 end;