diff -r 0467dd0d66ff -r 9df44a4f1bf7 TFL/rules.sml
--- a/TFL/rules.sml	Thu May 18 11:40:57 2000 +0200
+++ b/TFL/rules.sml	Thu May 18 11:43:57 2000 +0200
@@ -427,7 +427,7 @@
   let val {prop, ...} = rep_thm thm
   in case prop 
      of (Const("==>",_)$(Const("Trueprop",_)$ _) $
-         (Const("==",_) $ (Const ("cut",_) $ f $ R $ a $ x) $ _)) => false
+         (Const("==",_) $ (Const ("WF.cut",_) $ f $ R $ a $ x) $ _)) => false
       | _ => true
   end;
 
@@ -631,7 +631,7 @@
   end;
 
 fun restricted t = is_some (S.find_term
-			    (fn (Const("cut",_)) =>true | _ => false) 
+			    (fn (Const("WF.cut",_)) =>true | _ => false) 
 			    t)
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =