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