src/Pure/primitive_defs.ML
changeset 64596 51f8e259de50
parent 63395 734723445a8c
child 67721 5348bea4accd
--- 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 [];