1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Feb 08 13:20:40 2018 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Fri Feb 09 11:16:05 2018 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4  ML {*
     1.5    val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
     1.6    val (_, denom) = 
     1.7 -    HOLogic.dest_bin "Fields.inverse_class.divide" (type_of expr) expr;
     1.8 +    HOLogic.dest_bin "Rings.divide_class.divide" (type_of expr) expr;
     1.9    term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
    1.10  *}
    1.11  
    1.12 @@ -216,7 +216,7 @@
    1.13   *)
    1.14  fun eval_get_denominator (thmid:string) _ 
    1.15  		      (t as Const ("Rational.get_denominator", _) $
    1.16 -              (Const ("Fields.inverse_class.divide", _) $num 
    1.17 +              (Const ("Rings.divide_class.divide", _) $num 
    1.18                  $denom)) thy = 
    1.19          SOME (mk_thmid thmid "" (term_to_string''' thy denom) "", 
    1.20  	        Trueprop $ (mk_equality (t, denom)))
    1.21 @@ -236,7 +236,7 @@
    1.22   *)
    1.23  fun eval_get_numerator (thmid:string) _ 
    1.24  		      (t as Const ("Rational.get_numerator", _) $
    1.25 -              (Const ("Fields.inverse_class.divide", _) $num
    1.26 +              (Const ("Rings.divide_class.divide", _) $num
    1.27                  $denom )) thy = 
    1.28          SOME (mk_thmid thmid "" (term_to_string''' thy num) "", 
    1.29  	        Trueprop $ (mk_equality (t, num)))
    1.30 @@ -589,7 +589,7 @@
    1.31    val SOME numerator = parseNEW ctxt "3::real";
    1.32  
    1.33    val expr' = HOLogic.mk_binop
    1.34 -    "Fields.inverse_class.divide" (numerator, denominator');
    1.35 +    "Rings.divide_class.divide" (numerator, denominator');
    1.36    term2str expr';
    1.37  *}
    1.38