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.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
```