src/Pure/thm.ML

   orient_comb_simps del_rrule (map mk_rrule2 o mk_rrule mss) (mss,thms);
 
 
 (* add_congs *)
 
-(*FIXME -> term.ML *)
-fun is_Bound (Bound _) = true
-fun is_Bound _         = false;
-
 fun is_full_cong_prems [] varpairs = null varpairs
   | is_full_cong_prems (p::prems) varpairs =
     (case Logic.strip_assums_concl p of
        Const("==",_) $ lhs $ rhs =>
          let val (x,xs) = strip_comb lhs and (y,ys) = strip_comb rhs
          in is_Var x  andalso  forall is_Bound xs  andalso
             null(findrep(xs))  andalso xs=ys andalso
             (x,y) mem varpairs andalso
-            is_full_cong_prems (p::prems) (varpairs\(x,y))
+            is_full_cong_prems prems (varpairs\(x,y))
          end
      | _ => false);
 
 fun is_full_cong (Thm{prop,...}) =
 let val prems = Logic.strip_imp_prems prop