1.1 --- a/src/HOL/Tools/TFL/tfl.ML	Tue Oct 20 23:25:04 2009 +0200
     1.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 00:36:12 2009 +0200
     1.3 @@ -724,7 +724,7 @@
     1.4  in
     1.5  fun build_ih f P (pat,TCs) =
     1.6   let val globals = S.free_vars_lr pat
     1.7 -     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
     1.8 +     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
     1.9       fun dest_TC tm =
    1.10           let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
    1.11               val (R,y,_) = S.dest_relation R_y_pat
    1.12 @@ -753,7 +753,7 @@
    1.13  fun build_ih f (P,SV) (pat,TCs) =
    1.14   let val pat_vars = S.free_vars_lr pat
    1.15       val globals = pat_vars@SV
    1.16 -     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
    1.17 +     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
    1.18       fun dest_TC tm =
    1.19           let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
    1.20               val (R,y,_) = S.dest_relation R_y_pat
    1.21 @@ -786,7 +786,7 @@
    1.22   let val tych = Thry.typecheck thy
    1.23       val antc = tych(#ant(S.dest_imp tm))
    1.24       val thm' = R.SPEC_ALL thm
    1.25 -     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
    1.26 +     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
    1.27       fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
    1.28       fun mk_ih ((TC,locals),th2,nested) =
    1.29           R.GENL (map tych locals)