# HG changeset patch
# User wenzelm
# Date 1194470411 -3600
# Node ID 73491e84ead102f7ff73f09cd69274ff28143073
# Parent  73072178e0cec0dfa59fec08d5c0fff5657b5d63
export read_const';
tuned;

diff -r 73072178e0ce -r 73491e84ead1 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Nov 07 22:20:09 2007 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Nov 07 22:20:11 2007 +0100
@@ -55,6 +55,7 @@
   val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
   val read_tyname: Proof.context -> string -> typ
+  val read_const': Proof.context -> string -> term
   val read_const: Proof.context -> string -> term
   val decode_term: Proof.context -> term -> term
   val read_term_pattern: Proof.context -> string -> term
@@ -985,9 +986,7 @@
 
 fun const_ast_tr intern ctxt [Syntax.Variable c] =
       let
-        val consts = consts_of ctxt;
-        val c' = Consts.intern consts c;
-        val _ = Consts.the_constraint consts c' handle TYPE (msg, _, _) => error msg;
+        val Const (c', _) = read_const' ctxt c;
         val d = if intern then const_syntax_name ctxt c' else c;
       in Syntax.Constant d end
   | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);