# HG changeset patch
# User wenzelm
# Date 1162896410 -3600
# Node ID 62ccdaf9369a1e616943d5dca7c7dadff919e6b7
# Parent  cef082634be9d98716be71453b942f4a63dc6f38
replaced const_syntax by notation, which operates on terms;
read_const: include type;

diff -r cef082634be9 -r 62ccdaf9369a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Nov 07 11:46:49 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Nov 07 11:46:50 2006 +0100
@@ -138,7 +138,8 @@
   val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
   val get_case: Proof.context -> string -> string option list -> RuleCases.T
   val expand_abbrevs: bool -> Proof.context -> Proof.context
-  val add_const_syntax: Syntax.mode -> (string * mixfix) list -> Proof.context -> Proof.context
+  val add_notation: Syntax.mode -> (term * mixfix) list ->
+    Proof.context -> Proof.context
   val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list ->
     Proof.context -> Proof.context
   val verbose: bool ref
@@ -554,7 +555,7 @@
 
 fun read_const ctxt c =
   (case lookup_skolem ctxt c of
-    SOME c' => Free (c', dummyT)
+    SOME x => Free (x, infer_type ctxt x)
   | NONE => Consts.read_const (consts_of ctxt) c);
 
 
@@ -839,10 +840,13 @@
 
 (* authentic constants *)
 
-fun add_const_syntax prmode args ctxt =
+fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx))
+  | const_syntax ctxt (Const (c, _), mx) = SOME (false, Consts.syntax (consts_of ctxt) (c, mx))
+  | const_syntax _ _ = NONE;
+
+fun add_notation prmode args ctxt =
   ctxt |> map_syntax
-    (LocalSyntax.add_modesyntax (theory_of ctxt) prmode
-      (map (pair false o Consts.syntax (consts_of ctxt)) args));
+    (LocalSyntax.add_modesyntax (theory_of ctxt) prmode (map_filter (const_syntax ctxt) args));
 
 fun context_const_ast_tr context [Syntax.Variable c] =
       let