TFL/rules.sml
changeset 10212 33fe2d701ddd
parent 10117 8e58b3045e29
child 10417 42e6b8502d52
     1.1 --- a/TFL/rules.sml	Thu Oct 12 18:09:06 2000 +0200
     1.2 +++ b/TFL/rules.sml	Thu Oct 12 18:38:23 2000 +0200
     1.3 @@ -482,7 +482,7 @@
     1.4    let val {prop, ...} = rep_thm thm
     1.5    in case prop 
     1.6       of (Const("==>",_)$(Const("Trueprop",_)$ _) $
     1.7 -         (Const("==",_) $ (Const ("WF.cut",_) $ f $ R $ a $ x) $ _)) => false
     1.8 +         (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
     1.9        | _ => true
    1.10    end;
    1.11  
    1.12 @@ -685,7 +685,7 @@
    1.13    end;
    1.14  
    1.15  fun restricted t = is_some (S.find_term
    1.16 -			    (fn (Const("WF.cut",_)) =>true | _ => false) 
    1.17 +			    (fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false) 
    1.18  			    t)
    1.19  
    1.20  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =