src/HOL/Import/shuffler.ML

--- a/src/HOL/Import/shuffler.ML	Fri Apr 02 17:40:32 2004 +0200
+++ b/src/HOL/Import/shuffler.ML	Sun Apr 04 15:34:14 2004 +0200
@@ -263,7 +263,8 @@
 		  (([],tfree_names),tvars)
 	val t' = subst_TVars type_inst t
     in
-	(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))) type_inst)
+	(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
+		  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
     end
 
 fun inst_tfrees sg [] thm = thm