src/Pure/ProofGeneral/proof_general_emacs.ML
changeset 43547 f3a8476285c6
parent 40133 b61d52de66f0
child 43548 f231a7594e54
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jun 25 15:08:58 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jun 25 17:17:49 2011 +0200
@@ -41,6 +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.hiliteN then (special "0", special "1")
           else if name = Markup.tclassN then (special "B", special "A")
           else if name = Markup.tfreeN then (special "C", special "A")