ProofContext.read_const: allow for type constraint (for fixed variable);
added proof command 'write' to introduce concrete syntax within a proof body;

--- a/etc/isar-keywords-ZF.el	Thu Apr 29 16:53:08 2010 +0200
+++ b/etc/isar-keywords-ZF.el	Thu Apr 29 16:55:22 2010 +0200
@@ -210,6 +210,7 @@
     "using"
     "welcome"
     "with"
+    "write"
     "{"
     "}"))
 
@@ -486,7 +487,8 @@
     "txt"
     "txt_raw"
     "unfolding"
-    "using"))
+    "using"
+    "write"))
 
 (defconst isar-keywords-proof-asm
   '("assume"

--- a/etc/isar-keywords.el	Thu Apr 29 16:53:08 2010 +0200
+++ b/etc/isar-keywords.el	Thu Apr 29 16:55:22 2010 +0200
@@ -273,6 +273,7 @@
     "values"
     "welcome"
     "with"
+    "write"
     "{"
     "}"))
 
@@ -628,7 +629,8 @@
     "txt"
     "txt_raw"
     "unfolding"
-    "using"))
+    "using"
+    "write"))
 
 (defconst isar-keywords-proof-asm
   '("assume"

--- a/src/Pure/Isar/args.ML	Thu Apr 29 16:53:08 2010 +0200
+++ b/src/Pure/Isar/args.ML	Thu Apr 29 16:55:22 2010 +0200
@@ -205,7 +205,7 @@
   >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
 
 fun const strict =
-  Scan.peek (fn ctxt => named_term (ProofContext.read_const (Context.proof_of ctxt) strict))
+  Scan.peek (fn ctxt => named_term (ProofContext.read_const (Context.proof_of ctxt) strict dummyT))
   >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
 
 fun const_proper strict =

--- a/src/Pure/Isar/isar_syn.ML	Thu Apr 29 16:53:08 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 29 16:55:22 2010 +0200
@@ -225,22 +225,22 @@
     >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
 
 val _ =
-  OuterSyntax.local_theory "type_notation" "add notation for type constructors" K.thy_decl
+  OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors" K.thy_decl
     (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
     >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
 
 val _ =
-  OuterSyntax.local_theory "no_type_notation" "delete notation for type constructors" K.thy_decl
+  OuterSyntax.local_theory "no_type_notation" "delete concrete syntax for type constructors" K.thy_decl
     (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
     >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
 
 val _ =
-  OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl
+  OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables" K.thy_decl
     (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
     >> (fn (mode, args) => Specification.notation_cmd true mode args));
 
 val _ =
-  OuterSyntax.local_theory "no_notation" "delete notation for constants / fixed variables" K.thy_decl
+  OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables" K.thy_decl
     (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
     >> (fn (mode, args) => Specification.notation_cmd false mode args));
 
@@ -615,6 +615,12 @@
     (P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
       >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
 
+val _ =
+  OuterSyntax.command "write" "add concrete syntax for constants / fixed variables"
+    (K.tag_proof K.prf_decl)
+    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
+    >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
+
 val case_spec =
   (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
     P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1;

--- a/src/Pure/Isar/proof.ML	Thu Apr 29 16:53:08 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Apr 29 16:55:22 2010 +0200
@@ -43,6 +43,8 @@
   val simple_goal: state -> {context: context, goal: thm}
   val let_bind: (term list * term) list -> state -> state
   val let_bind_cmd: (string list * string) list -> state -> state
+  val write: Syntax.mode -> (term * mixfix) list -> state -> state
+  val write_cmd: Syntax.mode -> (string * mixfix) list -> state -> state
   val fix: (binding * typ option * mixfix) list -> state -> state
   val fix_cmd: (binding * string option * mixfix) list -> state -> state
   val assm: Assumption.export ->
@@ -539,6 +541,24 @@
 end;
 
 
+(* concrete syntax *)
+
+local
+
+fun gen_write prep_arg mode args = map_context (fn ctxt =>
+  ctxt |> ProofContext.notation true mode (map (prep_arg ctxt) args));
+
+in
+
+val write = gen_write (K I);
+
+val write_cmd =
+  gen_write (fn ctxt => fn (c, mx) =>
+    (ProofContext.read_const ctxt false (Syntax.mixfixT mx) c, mx));
+
+end;
+
+
 (* fix *)
 
 local

--- a/src/Pure/Isar/proof_context.ML	Thu Apr 29 16:53:08 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Apr 29 16:55:22 2010 +0200
@@ -55,13 +55,13 @@
   val cert_typ_abbrev: Proof.context -> typ -> typ
   val get_skolem: Proof.context -> string -> string
   val revert_skolem: Proof.context -> string -> string
-  val infer_type: Proof.context -> string -> typ
+  val infer_type: Proof.context -> string * typ -> typ
   val inferred_param: string -> Proof.context -> typ * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
   val read_type_name: Proof.context -> bool -> string -> typ
   val read_type_name_proper: Proof.context -> bool -> string -> typ
   val read_const_proper: Proof.context -> bool -> string -> term
-  val read_const: Proof.context -> bool -> string -> term
+  val read_const: Proof.context -> bool -> typ -> string -> term
   val allow_dummies: Proof.context -> Proof.context
   val check_tvar: Proof.context -> indexname * sort -> indexname * sort
   val check_tfree: Proof.context -> string * sort -> string * sort
@@ -438,11 +438,10 @@
 (* inferred types of parameters *)
 
 fun infer_type ctxt x =
-  Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt))
-    (Free (x, dummyT)));
+  Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x));
 
 fun inferred_param x ctxt =
-  let val T = infer_type ctxt x
+  let val T = infer_type ctxt (x, dummyT)
   in (T, ctxt |> Variable.declare_term (Free (x, T))) end;
 
 fun inferred_fixes ctxt =
@@ -505,13 +504,13 @@
 
 fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
 
-fun read_const ctxt strict text =
+fun read_const ctxt strict ty text =
   let val (c, pos) = token_content text in
     (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
       (SOME x, false) =>
         (Position.report (Markup.name x
             (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
-          Free (x, infer_type ctxt x))
+          Free (x, infer_type ctxt (x, ty)))
     | _ => prep_const_proper ctxt strict (c, pos))
   end;
 

--- a/src/Pure/Isar/specification.ML	Thu Apr 29 16:53:08 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Apr 29 16:55:22 2010 +0200
@@ -284,7 +284,7 @@
 val type_notation_cmd = gen_type_notation (fn ctxt => ProofContext.read_type_name ctxt false);
 
 val notation = gen_notation (K I);
-val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false);
+val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false dummyT);
 
 end;