src/Pure/envir.ML

 	| normT(TVar(v,_)) = (case assoc(iTs,v) of
 		Some(U) => normTh U
 	      | 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)) =
 	    (case xsearch(asol,w) of
 		Some u => normh u