1.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy	Thu Feb 08 13:20:40 2018 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy	Fri Feb 09 11:16:05 2018 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4   *)
     1.5  fun eval_get_denominator (thmid:string) _ 
     1.6  		      (t as Const ("Rational.get_denominator", _) $
     1.7 -              (Const ("Fields.inverse_class.divide", _) $num 
     1.8 +              (Const ("Rings.divide_class.divide", _) $num 
     1.9                  $denom)) thy = 
    1.10          SOME (mk_thmid thmid "" (term_to_string''' thy denom) "", 
    1.11  	        Trueprop $ (mk_equality (t, denom)))