# HG changeset patch
# User wenzelm
# Date 1519584218 -3600
# Node ID e6cd1fd4eb1980480703f7a2205d7cc827ff6924
# Parent  63e305429f8a356fd518424e77c3cd35e249a72f
prefer symbols;

diff -r 63e305429f8a -r e6cd1fd4eb19 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Feb 25 19:30:55 2018 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Feb 25 19:43:38 2018 +0100
@@ -472,7 +472,7 @@
    one of the premises. Unfortunately, this sometimes yields "Variable
    has two distinct types" errors. To avoid this, we instantiate the
    variables before applying "assume_tac". Typical constraints are of the form
-     ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x,
+     ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z \<equiv>\<^sup>? SK_a_b_c_x,
    where the nonvariables are goal parameters. *)
 fun unify_first_prem_with_concl ctxt i th =
   let
diff -r 63e305429f8a -r e6cd1fd4eb19 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Feb 25 19:30:55 2018 +0100
+++ b/src/Pure/more_thm.ML	Sun Feb 25 19:43:38 2018 +0100
@@ -705,7 +705,7 @@
 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
 
 fun pretty_flexpair ctxt (t, u) = Pretty.block
-  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
+  [Syntax.pretty_term ctxt t, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, Syntax.pretty_term ctxt u];
 
 fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
   let
diff -r 63e305429f8a -r e6cd1fd4eb19 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Sun Feb 25 19:30:55 2018 +0100
+++ b/src/Pure/unify.ML	Sun Feb 25 19:43:38 2018 +0100
@@ -243,7 +243,7 @@
 (*flexflex: the flex-flex pairs,  flexrigid: the flex-rigid pairs
   Does not perform assignments for flex-flex pairs:
     may create nonrigid paths, which prevent other assignments.
-  Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
+  Does not even identify Vars in dpairs such as ?a \<equiv>\<^sup>? ?b; an attempt to
     do so caused numerous problems with no compensating advantage.
 *)
 fun SIMPL0 context dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list =
@@ -426,7 +426,7 @@
 
 (*If an argument contains a banned Bound, then it should be deleted.
   But if the only path is flexible, this is difficult; the code gives up!
-  In \<lambda>x y. ?a x =?= \<lambda>x y. ?b (?c y) should we instantiate ?b or ?c *)
+  In \<lambda>x y. ?a x \<equiv>\<^sup>? \<lambda>x y. ?b (?c y) should we instantiate ?b or ?c *)
 exception CHANGE_FAIL;   (*flexible occurrence of banned variable, or other reason to quit*)
 
 
@@ -580,7 +580,7 @@
           val ctxt = Context.proof_of context;
           fun termT t =
             Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
-          val prt = Pretty.blk (0, [termT u, Pretty.str " =?=", Pretty.brk 1, termT t]);
+          val prt = Pretty.blk (0, [termT u, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, termT t]);
         in tracing (Pretty.string_of prt) end;
     in tracing msg; List.app pdp dpairs end
   else ();