# HG changeset patch
# User wenzelm
# Date 1662578110 -7200
# Node ID 47413d778c5f5014e2897e30f17b93b557a3e7d3
# Parent  1600fb749c54b0c9a146d51ad66a4653a4e5eba4
clarified output;

diff -r 1600fb749c54 -r 47413d778c5f src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Sep 07 11:43:34 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Sep 07 21:15:10 2022 +0200
@@ -252,7 +252,7 @@
 
 fun pretty_goal_inst ctxt propss goal =
   let
-    val title = "instantiation:";
+    val title = "goal instantiation:";
 
     fun prt_inst env =
       if Envir.is_empty env then []
@@ -275,12 +275,12 @@
               val t' = Envir.subst_term (tyenv, tenv) (Envir.subst_term_types tyenv t);
             in if t aconv t' then NONE else SOME (prt_term t, prt_term t') end;
 
-          fun prt_eq (x, y) = Pretty.block [x, Pretty.str " =", Pretty.brk 1, y];
+          fun inst_pair (x, y) = Pretty.item [x, Pretty.str " \<leadsto>", Pretty.brk 1, y];
 
           val prts =
             ((fold o fold) Term.add_tvars propss [] |> sort Term_Ord.tvar_ord |> map_filter instT) @
             ((fold o fold) Term.add_vars propss [] |> sort Term_Ord.var_ord |> map_filter inst);
-        in if null prts then [] else [Pretty.big_list title (map prt_eq prts)] end;
+        in if null prts then [] else [Pretty.big_list title (map inst_pair prts)] end;
 
     fun prt_failed prt = [Pretty.block [Pretty.str title, Pretty.brk 1, prt]];