# HG changeset patch
# User wenzelm
# Date 1303242942 -7200
# Node ID 282b7a3065d3c9055ddb407430ad93d183f4af89
# Parent  5b9dd52f5dca6849cf7b5de158dee2748ec1d3b8
explicit markup for loose bounds;

diff -r 5b9dd52f5dca -r 282b7a3065d3 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Apr 19 21:33:56 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Apr 19 21:55:42 2011 +0200
@@ -623,7 +623,7 @@
 (* basic syntax *)
 
 val token_markers =
-  ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"];
+  ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
 
 val basic_nonterms =
   (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
diff -r 5b9dd52f5dca -r 282b7a3065d3 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Apr 19 21:33:56 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Apr 19 21:55:42 2011 +0200
@@ -464,7 +464,7 @@
       | ast_of (t as _ $ _) =
           let val (f, args) = strip_comb t
           in Ast.mk_appl (ast_of f) (map ast_of args) end
-      | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
+      | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)]
       | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
   in ast_of end;
 
@@ -610,6 +610,7 @@
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
       | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
       | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
+      | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.malformed, x))
       | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
       | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
       | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))