--- a/TFL/rules.sml Thu Oct 12 18:09:06 2000 +0200
+++ b/TFL/rules.sml Thu Oct 12 18:38:23 2000 +0200
@@ -482,7 +482,7 @@
let val {prop, ...} = rep_thm thm
in case prop
of (Const("==>",_)$(Const("Trueprop",_)$ _) $
- (Const("==",_) $ (Const ("WF.cut",_) $ f $ R $ a $ x) $ _)) => false
+ (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
| _ => true
end;
@@ -685,7 +685,7 @@
end;
fun restricted t = is_some (S.find_term
- (fn (Const("WF.cut",_)) =>true | _ => false)
+ (fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false)
t)
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =