--- a/src/HOL/Algebra/ringsimp.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Tue Oct 09 00:20:13 2007 +0200
@@ -34,7 +34,7 @@
fun print_structures ctxt =
let
val structs = Data.get (Context.Proof ctxt);
- val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
+ val pretty_term = Pretty.quote o Syntax.pretty_term ctxt;
fun pretty_struct ((s, ts), _) = Pretty.block
[Pretty.str s, Pretty.str ":", Pretty.brk 1,
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];