# HG changeset patch
# User wenzelm
# Date 1348942430 -7200
# Node ID de6be6922c19aa381feea366baf275e7eb614dec
# Parent  ac48def96b697e5cbdfb7b4ca217309bc3c2673b
proper handling of constraints stemming from idtyp_ast_tr';

diff -r ac48def96b69 -r de6be6922c19 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 19:28:03 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 20:13:50 2012 +0200
@@ -641,15 +641,18 @@
       | token_trans _ _ = NONE;
 
     fun markup_trans a [Ast.Variable x] = token_trans a x
-      | markup_trans "_constrain" [t, ty] =
-          if not show_types andalso show_markup then
-            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
-          else NONE
+      | markup_trans "_constrain" [t, ty] = constrain_trans t ty
+      | markup_trans "_idtyp" [t, ty] = constrain_trans t ty
       | markup_trans _ _ = NONE
 
+    and constrain_trans t ty =
+      if not show_types andalso show_markup then
+        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
+      else NONE
+
     and pretty_typ_ast m ast = ast
       |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern
       |> Pretty.markup m