src/Pure/Syntax/syntax_phases.ML

       end;
   in
     tm
     |> mark_aprop
     |> show_types ? prune_types ctxt
+    |> Variable.revert_bounds ctxt
     |> mark_atoms idents is_syntax_const ctxt
     |> ast_of
   end;
 
 end;