src/Pure/PIDE/resources.ML
changeset 58741 6e7b009e6d94
parent 58716 23a380cc45f4
child 58849 ef7700ecce83
     1.1 --- a/src/Pure/PIDE/resources.ML	Mon Oct 20 23:17:28 2014 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Tue Oct 21 09:50:22 2014 +0200
     1.3 @@ -224,7 +224,7 @@
     1.4      space_explode "/" name
     1.5      |> map Latex.output_ascii
     1.6      |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
     1.7 -    |> Thy_Output.enclose_isabelle_tt ctxt
     1.8 +    |> enclose "\\isatt{" "}"
     1.9    end;
    1.10  
    1.11  in