src/Pure/Pure.thy
changeset 64677 8dc24130e8fe
parent 64595 511b30aa4100
child 66194 8d34d42c40cb
     1.1 --- a/src/Pure/Pure.thy	Tue Dec 27 17:33:57 2016 +0100
     1.2 +++ b/src/Pure/Pure.thy	Wed Dec 28 10:39:50 2016 +0100
     1.3 @@ -991,7 +991,7 @@
     1.4  local
     1.5  
     1.6  fun report_back () =
     1.7 -  Output.report [Markup.markup Markup.bad "Explicit backtracking"];
     1.8 +  Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
     1.9  
    1.10  val _ =
    1.11    Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"