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'