1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex	Fri Oct 12 16:03:07 2012 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex	Fri Oct 12 17:06:58 2012 +0200
     1.3 @@ -338,7 +338,7 @@
     1.4  \isatagML
     1.5  \isacommand{ML}\isamarkupfalse%
     1.6  \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
     1.7 -\ \ val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ ProofContext{\isaliteral{2E}{\isachardot}}init{\isaliteral{5F}{\isacharunderscore}}global\ %
     1.8 +\ \ val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ Proof_Context{\isaliteral{2E}{\isachardot}}init{\isaliteral{5F}{\isacharunderscore}}global\ %
     1.9  \isaantiq
    1.10  theory\ Isac{}%
    1.11  \endisaantiq
    1.12 @@ -2686,7 +2686,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 } ;
    1.17 +      val ctxt = Proof_Context.init_global @ { theory } ;
    1.18        val SOME t = 
    1.19          parseNEW ctxt "(num_orig::real) = 
    1.20                            get_numerator(rhs f_f)";