1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Fri Oct 12 16:03:07 2012 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Fri Oct 12 17:06:58 2012 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4  text{*\noindent We try two different notations and check which of them 
     1.5         Isabelle can handle best.*}
     1.6  ML {*
     1.7 -  val ctxt = ProofContext.init_global @{theory};
     1.8 +  val ctxt = Proof_Context.init_global @{theory};
     1.9    val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
    1.10  
    1.11    val SOME fun1 = 
    1.12 @@ -1614,7 +1614,7 @@
    1.13       \item Then we add line by line. Already the first line causes the error. 
    1.14          So we investigate it by
    1.15        \begin{verbatim}
    1.16 -      val ctxt = ProofContext.init_global @{theory "Inverse_Z_Transform"} ;
    1.17 +      val ctxt = Proof_Context.init_global @{theory "Inverse_Z_Transform"} ;
    1.18        val SOME t = 
    1.19          parseNEW ctxt "(num_orig::real) = 
    1.20                            get_numerator(rhs f_f)";