In-lined the one function call to normTsh

--- a/src/Pure/envir.ML	Wed Nov 13 10:38:08 1996 +0100
+++ b/src/Pure/envir.ML	Wed Nov 13 10:41:50 1996 +0100
@@ -181,9 +181,8 @@
 	      | None => raise SAME)
       and normTh T = ((normT T) handle SAME => T)
       and normTs([]) = raise SAME
-	| normTs(T::Ts) = ((normT T :: normTsh Ts)
+	| normTs(T::Ts) = ((normT T :: (normTs Ts handle SAME => Ts))
 			   handle SAME => T :: normTs Ts)
-      and normTsh Ts = ((normTs Ts) handle SAME => Ts)
       and norm(Const(a,T)) = Const(a, normT T)
 	| norm(Free(a,T)) = Free(a, normT T)
 	| norm(Var (w,T)) =