src/FOL/simpdata.ML
 changeset 3537 79ac9b475621 parent 3206 a3de7f32728c child 3566 c9c351374651
```     1.1 --- a/src/FOL/simpdata.ML	Fri Jul 18 14:06:54 1997 +0200
1.2 +++ b/src/FOL/simpdata.ML	Tue Jul 22 11:12:55 1997 +0200
1.3 @@ -257,18 +257,21 @@
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 +local
1.9    fun is_eq (Const ("Trueprop", _) \$ (Const("op ="  ,_) \$ _ \$ _)) = true
1.10 -  |   is_eq (Const ("Trueprop", _) \$ (Const("op <->",_) \$ _ \$ _)) = true
1.11 -  |   is_eq _ = false;
1.12 +    | is_eq (Const ("Trueprop", _) \$ (Const("op <->",_) \$ _ \$ _)) = true
1.13 +    | is_eq _ = false;
1.14    fun find_eq n [] = None
1.15 -  |   find_eq n (t :: ts) = if (is_eq t) then Some n else find_eq (n + 1) ts;
1.16 -  fun rot_eq state = let val (_, _, Bi, _) = dest_state (state, i) in
1.17 -	    (case find_eq 0 (Logic.strip_assums_hyp Bi) of
1.18 -	      None   => no_tac
1.19 -	    | Some 0 => no_tac
1.20 -	    | Some n => rotate_tac n i) end;
1.21 -in STATE rot_eq end;
1.22 +    | find_eq n (t :: ts) = if (is_eq t) then Some n
1.23 +			    else find_eq (n + 1) ts;
1.24 +in
1.25 +val rot_eq_tac =
1.26 +     SUBGOAL (fn (Bi,i) =>
1.27 +	      case find_eq 0 (Logic.strip_assums_hyp Bi) of
1.28 +		  None   => no_tac
1.29 +		| Some 0 => no_tac
1.30 +		| Some n => rotate_tac n i)
1.31 +end;
1.32
1.33
1.34  fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN'
```