# HG changeset patch
# User wenzelm
# Date 1300738599 -3600
# Node ID fda09013c496da88bbe4ba6d61f407dbaba1482e
# Parent  17dc2c6edb937a58b447193590f4f3bcce1c714d
tuned;

diff -r 17dc2c6edb93 -r fda09013c496 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Mon Mar 21 21:05:08 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Mon Mar 21 21:16:39 2011 +0100
@@ -347,10 +347,8 @@
 
 (* idtyp constraints *)
 
-fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant c, x, ty], xs] =
-      if c = "_constrain" then
-        Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
-      else raise Match
+fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
+      Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
   | idtyp_ast_tr' _ _ = raise Match;