# HG changeset patch
# User paulson
# Date 848330854 -3600
# Node ID 58383908f1774487e243b93b25899129f535ebb8
# Parent  97a2d44a80138a3dec6604822d4c86c4a6b72eb4
Speedups involving norm

diff -r 97a2d44a8013 -r 58383908f177 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Mon Nov 18 16:26:43 1996 +0100
+++ b/src/Pure/envir.ML	Mon Nov 18 16:27:34 1996 +0100
@@ -160,17 +160,17 @@
 fun norm_term1 (asol,t) : term =
   let fun norm (Var (w,T)) =
 	    (case xsearch(asol,w) of
-		Some u => normh u
+		Some u => (norm u handle SAME => u)
 	      | None   => raise SAME)
 	| norm (Abs(a,T,body)) =  Abs(a, T, norm body)
-	| norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
+	| norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
 	| norm (f $ t) =
 	    ((case norm f of
-	       Abs(_,_,body) => normh(subst_bounds([t], body))
-	     | nf => nf $ normh t)
+	       Abs(_,_,body) => normh(subst_bound (t, body))
+	     | nf => nf $ (norm t handle SAME => t))
 	    handle SAME => f $ norm t)
 	| norm _ =  raise SAME
-      and normh t = (norm t) handle SAME => t
+      and normh t = norm t handle SAME => t
   in normh t end
 
 and norm_term2(asol,iTs,t) : term =
@@ -191,10 +191,10 @@
 	      | None   => Var(w,normT T))
 	| norm(Abs(a,T,body)) =
 	      (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
-	| norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
+	| norm(Abs(_,_,body) $ t) = normh(subst_bound (t, body))
 	| norm(f $ t) =
 	    ((case norm f of
-	       Abs(_,_,body) => normh(subst_bounds([t], body))
+	       Abs(_,_,body) => normh(subst_bound (t, body))
 	     | nf => nf $ normh t)
 	    handle SAME => f $ norm t)
 	| norm _ =  raise SAME