Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Syntax/syntax_phases.ML
changeset 61864 3a5992c3410c
parent 61077 06cca32aa519
child 62239 6ee95b93fbed 
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Dec 19 10:59:14 2015 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Dec 19 14:47:52 2015 +0100
@@ -750,7 +750,7 @@
         let
           val ((bg1, bg2), en) = typing_elem;
           val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
-        in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end
+        in SOME (Pretty.make_block (bg, en) false 0 [pretty_ast Markup.empty t]) end
       else NONE
 
     and ofsort_trans ty s =
@@ -758,7 +758,7 @@
         let
           val ((bg1, bg2), en) = sorting_elem;
           val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
-        in SOME (Pretty.raw_markup (bg, en) (0, [pretty_typ_ast Markup.empty ty])) end
+        in SOME (Pretty.make_block (bg, en) false 0 [pretty_typ_ast Markup.empty ty]) end
       else NONE
 
     and pretty_typ_ast m ast = ast
isabelle