--- a/TFL/rules.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/TFL/rules.ML Thu Mar 03 12:43:01 2005 +0100
@@ -133,7 +133,7 @@
fun FILTER_DISCH_ALL P thm =
let fun check tm = P (#t (Thm.rep_cterm tm))
- in foldr (fn (tm,th) => if check tm then DISCH tm th else th)
+ in Library.foldr (fn (tm,th) => if check tm then DISCH tm th else th)
(chyps thm, thm)
end;
@@ -658,7 +658,7 @@
in (ants,get_lhs eq)
end;
-fun restricted t = is_some (S.find_term
+fun restricted t = isSome (S.find_term
(fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false)
t)
@@ -785,7 +785,7 @@
val dummy = print_cterms "TC:"
[cterm_of sign (HOLogic.mk_Trueprop TC)]
val dummy = tc_list := (TC :: !tc_list)
- val nestedp = is_some (S.find_term is_func TC)
+ val nestedp = isSome (S.find_term is_func TC)
val dummy = if nestedp then say "nested" else say "not_nested"
val dummy = term_ref := ([func,TC]@(!term_ref))
val th' = if nestedp then raise RULES_ERR "solver" "nested function"
@@ -808,7 +808,7 @@
(prover names) (empty_ss addsimps [cut_lemma'] addeqcongs congs) ctm
val th2 = equal_elim th1 th
in
- (th2, filter (not o restricted) (!tc_list))
+ (th2, List.filter (not o restricted) (!tc_list))
end;