src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 27828 edafacb690a3
parent 27604 6c347b96d941
child 27860 5125b3c1efc2
equal deleted inserted replaced
27827:03ed3519cf48 27828:edafacb690a3
   246 
   246 
   247 val state_markup =
   247 val state_markup =
   248     split_markup (output_pgmltext (pgml PgipTypes.Display pgmlterms_no_text))
   248     split_markup (output_pgmltext (pgml PgipTypes.Display pgmlterms_no_text))
   249 
   249 
   250 val token_markups =
   250 val token_markups =
   251  [Markup.classN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
   251  [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
   252   Markup.boundN, Markup.varN, Markup.skolemN];
   252   Markup.boundN, Markup.varN, Markup.skolemN];
   253 
   253 
   254 in
   254 in
   255 
   255 
   256 val _ = Markup.add_mode proof_generalN (fn (markup as (name, _)) =>
   256 val _ = Markup.add_mode proof_generalN (fn (markup as (name, _)) =>