# HG changeset patch
# User paulson
# Date 847878110 -3600
# Node ID 9c2b4728641d53c36150062d456317c6654a0076
# Parent  934572a94139501e9470cebe0f9bcc829d54c659
In-lined the one function call to normTsh

diff -r 934572a94139 -r 9c2b4728641d src/Pure/envir.ML
--- 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)) =