--- a/src/HOL/Tools/TFL/rules.ML Tue Aug 02 10:36:50 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Tue Aug 02 11:52:57 2011 +0200
@@ -445,7 +445,7 @@
fun is_cong thm =
case (Thm.prop_of thm)
of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
- (Const("==",_) $ (Const (@{const_name Old_Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
+ (Const("==",_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) => false
| _ => true;
@@ -645,7 +645,7 @@
end;
fun restricted t = is_some (USyntax.find_term
- (fn (Const(@{const_name Old_Recdef.cut},_)) =>true | _ => false)
+ (fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false)
t)
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =