diff -r 869f50dfdad2 -r a93f496f6c30 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Jan 15 19:02:58 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Jan 15 22:24:57 2014 +0100
@@ -646,6 +646,7 @@
     tm
     |> mark_aprop
     |> show_types ? prune_types ctxt
+    |> Variable.revert_bounds ctxt
     |> mark_atoms idents is_syntax_const ctxt
     |> ast_of
   end;