asm_rewrite_goal_tac now calls SELECT_GOAL.
authorpaulson
Fri Nov 01 15:30:49 1996 +0100 (1996-11-01)
changeset 21455e8db0bc195e
parent 2144 ddb8499c772b
child 2146 6854b692f1fe
asm_rewrite_goal_tac now calls SELECT_GOAL.
Replaced min by Int.min
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Fri Nov 01 15:25:21 1996 +0100
     1.2 +++ b/src/Pure/tactic.ML	Fri Nov 01 15:30:49 1996 +0100
     1.3 @@ -455,9 +455,11 @@
     1.4      None => None
     1.5    | Some(thm,_) => Some(thm);
     1.6  
     1.7 -(*Rewrite subgoal i only *)
     1.8 -fun asm_rewrite_goal_tac mode prover_tac mss i =
     1.9 -      PRIMITIVE(rewrite_goal_rule mode (result1 prover_tac) mss i);
    1.10 +(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
    1.11 +fun asm_rewrite_goal_tac mode prover_tac mss =
    1.12 +      SELECT_GOAL 
    1.13 +        (PRIMITIVE
    1.14 +	   (rewrite_goal_rule mode (result1 prover_tac) mss 1));
    1.15  
    1.16  (*Rewrite throughout proof state. *)
    1.17  fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
    1.18 @@ -472,7 +474,7 @@
    1.19  
    1.20  (*The depth of nesting in a term*)
    1.21  fun term_depth (Abs(a,T,t)) = 1 + term_depth t
    1.22 -  | term_depth (f$t) = 1 + max [term_depth f, term_depth t]
    1.23 +  | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
    1.24    | term_depth _ = 0;
    1.25  
    1.26  val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm;