src/HOL/simpdata.ML
changeset 2805 6e5b2d6503eb
parent 2800 9741c4c6b62b
child 2935 998cb95fdd43
     1.1 --- a/src/HOL/simpdata.ML	Tue Mar 18 14:35:10 1997 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Tue Mar 18 15:11:02 1997 +0100
     1.3 @@ -364,17 +364,20 @@
     1.4  
     1.5  (* rot_eq_tac rotates the first equality premise of subgoal i to the front,
     1.6     fails if there is no equaliy or if an equality is already at the front *)
     1.7 -fun rot_eq_tac i = let
     1.8 -  fun is_eq (Const ("Trueprop", _) $ (Const("op =",_) $ _ $ _)) = true
     1.9 -  |   is_eq _ = false;
    1.10 -  fun find_eq n [] = None
    1.11 -  |   find_eq n (t :: ts) = if (is_eq t) then Some n else find_eq (n + 1) ts;
    1.12 -  fun rot_eq state = let val (_, _, Bi, _) = dest_state (state, i) in
    1.13 -	    (case find_eq 0 (Logic.strip_assums_hyp Bi) of
    1.14 -	      None   => no_tac
    1.15 -	    | Some 0 => no_tac
    1.16 -	    | Some n => rotate_tac n i) end;
    1.17 -in STATE rot_eq end;
    1.18 +fun rot_eq_tac i = 
    1.19 +  let fun is_eq (Const ("Trueprop", _) $ (Const("op =",_) $ _ $ _)) = true
    1.20 +	| is_eq _ = false;
    1.21 +      fun find_eq n [] = None
    1.22 +	| find_eq n (t :: ts) = if (is_eq t) then Some n 
    1.23 +				else find_eq (n + 1) ts;
    1.24 +      fun rot_eq state = 
    1.25 +	  let val (_, _, Bi, _) = dest_state (state, i) 
    1.26 +	  in  case find_eq 0 (Logic.strip_assums_hyp Bi) of
    1.27 +		  None   => no_tac
    1.28 +		| Some 0 => no_tac
    1.29 +		| Some n => rotate_tac n i
    1.30 +	  end;
    1.31 +  in STATE rot_eq end;
    1.32  
    1.33  (*an unsatisfactory fix for the incomplete asm_full_simp_tac!
    1.34    better: asm_really_full_simp_tac, a yet to be implemented version of
    1.35 @@ -423,10 +426,12 @@
    1.36  fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
    1.37  fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
    1.38  
    1.39 -fun auto_tac (cs,ss) = let val cs' = cs addss ss in
    1.40 -EVERY [	TRY (safe_tac cs'),
    1.41 -	REPEAT (FIRSTGOAL (fast_tac cs')),
    1.42 -	prune_params_tac] end;
    1.43 +fun auto_tac (cs,ss) = 
    1.44 +    let val cs' = cs addss ss 
    1.45 +    in  EVERY [TRY (safe_tac cs'),
    1.46 +	       REPEAT (FIRSTGOAL (fast_tac cs')),
    1.47 +	       prune_params_tac] 
    1.48 +    end;
    1.49  
    1.50  fun Auto_tac () = auto_tac (!claset, !simpset);
    1.51