# HG changeset patch
# User wenzelm
# Date 1309178338 -7200
# Node ID 844b4a178dffb2d34f388b69f8933e998ee0a1ad
# Parent  0d78c8d31d0d4c6269b79f45747c783228962560
markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";

diff -r 0d78c8d31d0d -r 844b4a178dff src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jun 27 09:42:46 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jun 27 14:38:58 2011 +0200
@@ -41,7 +41,7 @@
           if null ts then Markup.no_output
           else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
           else if name = Markup.sendbackN then (special "W", special "X")
-          else if name = Markup.bindingN then (special "F", special "A")
+          else if name = Markup.bindingN then (special "B", special "A")
           else if name = Markup.hiliteN then (special "0", special "1")
           else if name = Markup.tfreeN then (special "C", special "A")
           else if name = Markup.tvarN then (special "D", special "A")