diff -r 098c86e53153 -r 578a51fae383 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 05 14:25:18 2011 +0200
@@ -1093,12 +1093,12 @@
 
 local
 
-fun const_ast_tr intern ctxt [Syntax.Variable c] =
+fun const_ast_tr intern ctxt [Ast.Variable c] =
       let
         val Const (c', _) = read_const_proper ctxt false c;
         val d = if intern then Syntax.mark_const c' else c;
-      in Syntax.Constant d end
-  | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
+      in Ast.Constant d end
+  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
 
 val typ = Simple_Syntax.read_typ;