--- a/src/Pure/primitive_defs.ML Sun Dec 18 12:34:31 2016 +0100
+++ b/src/Pure/primitive_defs.ML Sun Dec 18 13:07:13 2016 +0100
@@ -34,7 +34,7 @@
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 (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
val lhs = Envir.beta_eta_contract raw_lhs;
val (head, args) = Term.strip_comb lhs;
val head_tfrees = Term.add_tfrees head [];