# HG changeset patch
# User paulson
# Date 934966443 -7200
# Node ID aad87acc8fa39f0e4cb6be9e038c37de87d89a84
# Parent  33058867d6eb7e5920d99b203dde8cb21877328a
freeze_thaw does nothing if no variables

diff -r 33058867d6eb -r aad87acc8fa3 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Aug 18 10:27:57 1999 +0200
+++ b/src/Pure/type.ML	Wed Aug 18 10:54:03 1999 +0200
@@ -134,8 +134,11 @@
     let val used = it_term_types add_typ_tfree_names (t, [])
 	and tvars = map #1 (it_term_types add_typ_tvars (t, []))
 	val (alist, _) = foldr newName (tvars, ([], used))
-    in  (map_term_types (map_type_tvar (freezeOne alist)) t,
-	 map_term_types (map_type_tfree (thawOne (map swap alist)))) 
+    in  
+	case alist of
+	    [] => (t, fn x=>x)      (*nothing to do!*)
+	  | _ =>  (map_term_types (map_type_tvar (freezeOne alist)) t,
+		   map_term_types (map_type_tfree (thawOne (map swap alist)))) 
     end;