# HG changeset patch
# User wenzelm
# Date 1394132108 -3600
# Node ID beef468837b14f09c80603e00ffad23042517a96
# Parent  c3b458435f4f07aff794fbe1887c347d323ae329
proper position for decode_pos, which is relevant for completion;

diff -r c3b458435f4f -r beef468837b1 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 17:37:32 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 19:55:08 2014 +0100
@@ -811,16 +811,15 @@
 
 (* authentic syntax *)
 
-fun const_ast_tr intern ctxt [Ast.Variable c] =
+fun const_ast_tr intern ctxt asts =
+  (case asts of
+    [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
       let
-        val (c', _) = decode_const ctxt (c, []);
+        val pos = the_default Position.none (Term_Position.decode p);
+        val (c', _) = decode_const ctxt (c, [pos]);
         val d = if intern then Lexicon.mark_const c' else c;
-      in Ast.Constant d end
-  | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =
-      (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
-        handle ERROR msg =>
-          error (msg ^ Position.here (the_default Position.none (Term_Position.decode pos))))
-  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
+      in Ast.Appl [Ast.Constant "_constrain", Ast.Constant d, T] end
+  | _ => raise Ast.AST ("const_ast_tr", asts));
 
 
 (* setup translations *)