--- a/src/HOLCF/Tools/pcpodef_package.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML Tue Oct 09 00:20:13 2007 +0200
@@ -67,7 +67,7 @@
val setT = Term.fastype_of set;
val rhs_tfrees = term_tfrees set;
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
- error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT));
+ error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
fun mk_nonempty A =
HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
fun mk_admissible A =