src/Pure/PIDE/resources.ML

--- a/src/Pure/PIDE/resources.ML	Mon Oct 20 23:17:28 2014 +0200
+++ b/src/Pure/PIDE/resources.ML	Tue Oct 21 09:50:22 2014 +0200
@@ -224,7 +224,7 @@
     space_explode "/" name
     |> map Latex.output_ascii
     |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
-    |> Thy_Output.enclose_isabelle_tt ctxt
+    |> enclose "\\isatt{" "}"
   end;
 
 in