1.1 --- a/src/Pure/Isar/locale.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -472,7 +472,7 @@
     1.4  fun print_registrations show_wits loc ctxt =
     1.5    let
     1.6      val thy = ProofContext.theory_of ctxt;
     1.7 -    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
     1.8 +    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     1.9      val prt_thm = prt_term o prop_of;
    1.10      fun prt_inst ts =
    1.11          Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
    1.12 @@ -1545,7 +1545,7 @@
    1.13  	| SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
    1.14              handle Termtab.DUP t =>
    1.15  	      error ("Conflicting interpreting equations for term " ^
    1.16 -		quote (ProofContext.string_of_term ctxt t))
    1.17 +		quote (Syntax.string_of_term ctxt t))
    1.18    in ((id', eqns'), eqns') end;
    1.19  
    1.20