# HG changeset patch
# User krauss
# Date 1209192571 -7200
# Node ID b53db47a43b4685b6f38854eaca404d700ddfed0
# Parent  397a1aeede7d7c7ca436b144504a94aee7c620a2
fixed recdef, broken by my previous commit

diff -r 397a1aeede7d -r b53db47a43b4 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Fri Apr 25 16:28:06 2008 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Sat Apr 26 08:49:31 2008 +0200
@@ -458,7 +458,7 @@
 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;
 
 
@@ -661,7 +661,7 @@
   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 =
diff -r 397a1aeede7d -r b53db47a43b4 src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Fri Apr 25 16:28:06 2008 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML	Sat Apr 26 08:49:31 2008 +0200
@@ -400,7 +400,7 @@
         end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
    else raise USYN_ERR "dest_relation" "not a boolean term";
 
-fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true
+fun is_WFR (Const(@{const_name "Wellfounded.wf"},_)$_) = true
   | is_WFR _                 = false;
 
 fun ARB ty = mk_select{Bvar=Free("v",ty),