src/Pure/primitive_defs.ML

     fun err msg = raise TERM (msg, [eq]);
     val eq_vars = Term.strip_all_vars eq;
     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 (==)";
     val lhs = Envir.beta_eta_contract raw_lhs;
     val (head, args) = Term.strip_comb lhs;