src/Tools/isac/Knowledge/Rational-WN.sml
changeset 59878 3163e63a5111
parent 59876 eff0b9fc6caa
child 59879 33449c96d99f
     1.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml	Wed Apr 15 11:37:43 2020 +0200
     1.3 @@ -199,7 +199,7 @@
     1.4  	     NONE => rew_once ruls asm ct apno thms
     1.5  	   | SOME (ct',asm') => 
     1.6  	     rew_once ruls (asm union asm') ct' Appl (rul::thms))
     1.7 -      | Rule.Num_Calc (cc as (op_,_)) => 
     1.8 +      | Rule.Eval (cc as (op_,_)) => 
     1.9  	  (case adhoc_thm thy cc ct of
    1.10  	       NONE => rew_once ruls asm ct apno thms
    1.11  	   | SOME (thmid, thm') => 
    1.12 @@ -235,7 +235,7 @@
    1.13  	     NONE => rew_once ruls asm ct apno thms
    1.14  	   | SOME (ct',asm') => 
    1.15  	     rew_once ruls (asm union asm') ct' Appl (rul::thms))
    1.16 -      | Rule.Num_Calc (cc as (op_,_)) => 
    1.17 +      | Rule.Eval (cc as (op_,_)) => 
    1.18  	  (case adhoc_thm thy cc ct of
    1.19  	       NONE => rew_once ruls asm ct apno thms
    1.20  	   | SOME (thmid, thm') =>