--- a/src/Pure/primitive_defs.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/primitive_defs.ML Fri Apr 08 13:31:16 2011 +0200
@@ -27,7 +27,7 @@
val eq_body = Term.strip_all_body eq;
val display_terms =
- commas_quote o map (Syntax.string_of_term ctxt o Syntax.bound_vars eq_vars);
+ commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";