diff -r ddb8499c772b -r 5e8db0bc195e src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Nov 01 15:25:21 1996 +0100
+++ b/src/Pure/tactic.ML	Fri Nov 01 15:30:49 1996 +0100
@@ -455,9 +455,11 @@
     None => None
   | Some(thm,_) => Some(thm);
 
-(*Rewrite subgoal i only *)
-fun asm_rewrite_goal_tac mode prover_tac mss i =
-      PRIMITIVE(rewrite_goal_rule mode (result1 prover_tac) mss i);
+(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
+fun asm_rewrite_goal_tac mode prover_tac mss =
+      SELECT_GOAL 
+        (PRIMITIVE
+	   (rewrite_goal_rule mode (result1 prover_tac) mss 1));
 
 (*Rewrite throughout proof state. *)
 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
@@ -472,7 +474,7 @@
 
 (*The depth of nesting in a term*)
 fun term_depth (Abs(a,T,t)) = 1 + term_depth t
-  | term_depth (f$t) = 1 + max [term_depth f, term_depth t]
+  | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
   | term_depth _ = 0;
 
 val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm;