src/HOL/Tools/TFL/rules.ML

 
 (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
 fun is_cong thm =
   case (Thm.prop_of thm)
      of (Const("==>",_)$(Const("Trueprop",_)$ _) $
-         (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
+         (Const("==",_) $ (Const (@{const_name "Wellfounded.cut"},_) $ f $ R $ a $ x) $ _)) => false
       | _ => true;
 
 
 fun dest_equal(Const ("==",_) $
                (Const ("Trueprop",_) $ lhs)

       val eq = Logic.strip_imp_concl tm
   in (ants,get_lhs eq)
   end;
 
 fun restricted t = isSome (S.find_term
-                            (fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false)
+                            (fn (Const(@{const_name "Wellfounded.cut"},_)) =>true | _ => false)
                             t)
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
  let val globals = func::G
      val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss