# HG changeset patch
# User wenzelm
# Date 1563716563 -7200
# Node ID 2adff54de67eb4adf58652b6d5dad5010d6ca610
# Parent  e31271559de844c454d3e49b9693980696a8d0ce
discontinued ASCII syntax;

diff -r e31271559de8 -r 2adff54de67e src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sun Jul 21 15:19:07 2019 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sun Jul 21 15:42:43 2019 +0200
@@ -1147,11 +1147,8 @@
   \begin{center}
   \begin{supertabular}{rclr}
 
-  @{syntax_def (inner) proof} & = & \<^verbatim>\<open>Lam\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\
-    & \<open>|\<close> & \<open>\<^bold>\<lambda>\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\
-    & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%\<close> \<open>any\<close> \\
+  @{syntax_def (inner) proof} & = & \<open>\<^bold>\<lambda>\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\
     & \<open>|\<close> & \<open>proof\<close> \<open>\<cdot>\<close> \<open>any\<close> \\
-    & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%%\<close> \<open>proof\<close> \\
     & \<open>|\<close> & \<open>proof\<close> \<open>\<bullet>\<close> \<open>proof\<close> \\
     & \<open>|\<close> & \<open>id  |  longid\<close> \\
   \\
diff -r e31271559de8 -r 2adff54de67e src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Sun Jul 21 15:19:07 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Jul 21 15:42:43 2019 +0200
@@ -53,10 +53,6 @@
      (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
      (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
      (Lexicon.mark_const "Pure.MinProof", proofT, Mixfix.mixfix "?")]
-  |> Sign.add_syntax (Print_Mode.ASCII, true)
-    [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)),
-     (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)),
-     (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))]
   |> Sign.add_trrules (map Syntax.Parse_Print_Rule
     [(Ast.mk_appl (Ast.Constant "_Lam")
         [Ast.mk_appl (Ast.Constant "_Lam0")