1.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml	Thu Oct 27 09:53:54 2016 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml	Thu Oct 27 10:48:10 2016 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4  	   | SOME (ct',asm') => 
     1.5  	     rew_once ruls (asm union asm') ct' Appl (rul::thms))
     1.6        | Calc (cc as (op_,_)) => 
     1.7 -	  (case get_calculation_ thy cc ct of
     1.8 +	  (case adhoc_thm thy cc ct of
     1.9  	       NONE => rew_once ruls asm ct apno thms
    1.10  	   | SOME (thmid, thm') => 
    1.11  	       let 
    1.12 @@ -236,7 +236,7 @@
    1.13  	   | SOME (ct',asm') => 
    1.14  	     rew_once ruls (asm union asm') ct' Appl (rul::thms))
    1.15        | Calc (cc as (op_,_)) => 
    1.16 -	  (case get_calculation_ thy cc ct of
    1.17 +	  (case adhoc_thm thy cc ct of
    1.18  	       NONE => rew_once ruls asm ct apno thms
    1.19  	   | SOME (thmid, thm') => 
    1.20  	       let