src/FOL/simpdata.ML
changeset 4188 1025a27b08f9
parent 4094 9e501199ec01
child 4189 b8c7a6bc6c16
     1.1 --- a/src/FOL/simpdata.ML	Fri Nov 07 17:51:26 1997 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Fri Nov 07 18:02:15 1997 +0100
     1.3 @@ -247,16 +247,11 @@
     1.4    fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
     1.5      | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
     1.6      | is_eq _ = false;
     1.7 -  fun find_eq n [] = None
     1.8 -    | find_eq n (t :: ts) = if (is_eq t) then Some n 
     1.9 -			    else find_eq (n + 1) ts;
    1.10 +  val find_eq = find_index is_eq;
    1.11  in
    1.12  val rot_eq_tac = 
    1.13 -     SUBGOAL (fn (Bi,i) => 
    1.14 -	      case find_eq 0 (Logic.strip_assums_hyp Bi) of
    1.15 -		  None   => no_tac
    1.16 -		| Some 0 => no_tac
    1.17 -		| Some n => rotate_tac n i)
    1.18 +     SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
    1.19 +		if n>0 then rotate_tac n i else no_tac end)
    1.20  end;
    1.21  
    1.22