1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Fri Oct 12 16:03:07 2012 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Fri Oct 12 17:06:58 2012 +0200
     1.3 @@ -73,8 +73,8 @@
     1.4              o Logic.strip_imp_concl) r';
     1.5  
     1.6  (*is displayed on top of <response> buffer...*)
     1.7 -Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
     1.8 -Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
     1.9 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
    1.10 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
    1.11  (**)
    1.12  
    1.13  "----------- test rewriting without Isac's thys ---------";
    1.14 @@ -90,7 +90,7 @@
    1.15  val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
    1.16    handle _ => error "rewrite.sml diff.behav. in rewriting";
    1.17  (*is displayed on _TOP_ of <response> buffer...*)
    1.18 -Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
    1.19 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
    1.20  if r = @{term "y*z + x::real"}
    1.21  then () else error "rewrite.sml diff.result in rewriting";
    1.22  
    1.23 @@ -108,7 +108,7 @@
    1.24  val NONE = (rewrite_ thy tord e_rls false thm tm)
    1.25    handle _ => error "rewrite.sml diff.behav. in rewriting";
    1.26  (*is displayed on _TOP_ of <response> buffer...*)
    1.27 -Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
    1.28 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
    1.29  
    1.30  val tm = @{term "x*y + z::real"};
    1.31  val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)