1.1 --- a/etc/isar-keywords-ZF.el	Thu Apr 29 16:53:08 2010 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Thu Apr 29 16:55:22 2010 +0200
     1.3 @@ -210,6 +210,7 @@
     1.4      "using"
     1.5      "welcome"
     1.6      "with"
     1.7 +    "write"
     1.8      "{"
     1.9      "}"))
    1.10  
    1.11 @@ -486,7 +487,8 @@
    1.12      "txt"
    1.13      "txt_raw"
    1.14      "unfolding"
    1.15 -    "using"))
    1.16 +    "using"
    1.17 +    "write"))
    1.18  
    1.19  (defconst isar-keywords-proof-asm
    1.20    '("assume"

     2.1 --- a/etc/isar-keywords.el	Thu Apr 29 16:53:08 2010 +0200
     2.2 +++ b/etc/isar-keywords.el	Thu Apr 29 16:55:22 2010 +0200
     2.3 @@ -273,6 +273,7 @@
     2.4      "values"
     2.5      "welcome"
     2.6      "with"
     2.7 +    "write"
     2.8      "{"
     2.9      "}"))
    2.10  
    2.11 @@ -628,7 +629,8 @@
    2.12      "txt"
    2.13      "txt_raw"
    2.14      "unfolding"
    2.15 -    "using"))
    2.16 +    "using"
    2.17 +    "write"))
    2.18  
    2.19  (defconst isar-keywords-proof-asm
    2.20    '("assume"

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

     4.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 29 16:53:08 2010 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 29 16:55:22 2010 +0200
     4.3 @@ -225,22 +225,22 @@
     4.4      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
     4.5  
     4.6  val _ =
     4.7 -  OuterSyntax.local_theory "type_notation" "add notation for type constructors" K.thy_decl
     4.8 +  OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors" K.thy_decl
     4.9      (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
    4.10      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
    4.11  
    4.12  val _ =
    4.13 -  OuterSyntax.local_theory "no_type_notation" "delete notation for type constructors" K.thy_decl
    4.14 +  OuterSyntax.local_theory "no_type_notation" "delete concrete syntax for type constructors" K.thy_decl
    4.15      (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
    4.16      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
    4.17  
    4.18  val _ =
    4.19 -  OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl
    4.20 +  OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables" K.thy_decl
    4.21      (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
    4.22      >> (fn (mode, args) => Specification.notation_cmd true mode args));
    4.23  
    4.24  val _ =
    4.25 -  OuterSyntax.local_theory "no_notation" "delete notation for constants / fixed variables" K.thy_decl
    4.26 +  OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables" K.thy_decl
    4.27      (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
    4.28      >> (fn (mode, args) => Specification.notation_cmd false mode args));
    4.29  
    4.30 @@ -615,6 +615,12 @@
    4.31      (P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
    4.32        >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
    4.33  
    4.34 +val _ =
    4.35 +  OuterSyntax.command "write" "add concrete syntax for constants / fixed variables"
    4.36 +    (K.tag_proof K.prf_decl)
    4.37 +    (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
    4.38 +    >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
    4.39 +
    4.40  val case_spec =
    4.41    (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
    4.42      P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1;

     5.1 --- a/src/Pure/Isar/proof.ML	Thu Apr 29 16:53:08 2010 +0200
     5.2 +++ b/src/Pure/Isar/proof.ML	Thu Apr 29 16:55:22 2010 +0200
     5.3 @@ -43,6 +43,8 @@
     5.4    val simple_goal: state -> {context: context, goal: thm}
     5.5    val let_bind: (term list * term) list -> state -> state
     5.6    val let_bind_cmd: (string list * string) list -> state -> state
     5.7 +  val write: Syntax.mode -> (term * mixfix) list -> state -> state
     5.8 +  val write_cmd: Syntax.mode -> (string * mixfix) list -> state -> state
     5.9    val fix: (binding * typ option * mixfix) list -> state -> state
    5.10    val fix_cmd: (binding * string option * mixfix) list -> state -> state
    5.11    val assm: Assumption.export ->
    5.12 @@ -539,6 +541,24 @@
    5.13  end;
    5.14  
    5.15  
    5.16 +(* concrete syntax *)
    5.17 +
    5.18 +local
    5.19 +
    5.20 +fun gen_write prep_arg mode args = map_context (fn ctxt =>
    5.21 +  ctxt |> ProofContext.notation true mode (map (prep_arg ctxt) args));
    5.22 +
    5.23 +in
    5.24 +
    5.25 +val write = gen_write (K I);
    5.26 +
    5.27 +val write_cmd =
    5.28 +  gen_write (fn ctxt => fn (c, mx) =>
    5.29 +    (ProofContext.read_const ctxt false (Syntax.mixfixT mx) c, mx));
    5.30 +
    5.31 +end;
    5.32 +
    5.33 +
    5.34  (* fix *)
    5.35  
    5.36  local

     6.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 29 16:53:08 2010 +0200
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 29 16:55:22 2010 +0200
     6.3 @@ -55,13 +55,13 @@
     6.4    val cert_typ_abbrev: Proof.context -> typ -> typ
     6.5    val get_skolem: Proof.context -> string -> string
     6.6    val revert_skolem: Proof.context -> string -> string
     6.7 -  val infer_type: Proof.context -> string -> typ
     6.8 +  val infer_type: Proof.context -> string * typ -> typ
     6.9    val inferred_param: string -> Proof.context -> typ * Proof.context
    6.10    val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
    6.11    val read_type_name: Proof.context -> bool -> string -> typ
    6.12    val read_type_name_proper: Proof.context -> bool -> string -> typ
    6.13    val read_const_proper: Proof.context -> bool -> string -> term
    6.14 -  val read_const: Proof.context -> bool -> string -> term
    6.15 +  val read_const: Proof.context -> bool -> typ -> string -> term
    6.16    val allow_dummies: Proof.context -> Proof.context
    6.17    val check_tvar: Proof.context -> indexname * sort -> indexname * sort
    6.18    val check_tfree: Proof.context -> string * sort -> string * sort
    6.19 @@ -438,11 +438,10 @@
    6.20  (* inferred types of parameters *)
    6.21  
    6.22  fun infer_type ctxt x =
    6.23 -  Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt))
    6.24 -    (Free (x, dummyT)));
    6.25 +  Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x));
    6.26  
    6.27  fun inferred_param x ctxt =
    6.28 -  let val T = infer_type ctxt x
    6.29 +  let val T = infer_type ctxt (x, dummyT)
    6.30    in (T, ctxt |> Variable.declare_term (Free (x, T))) end;
    6.31  
    6.32  fun inferred_fixes ctxt =
    6.33 @@ -505,13 +504,13 @@
    6.34  
    6.35  fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
    6.36  
    6.37 -fun read_const ctxt strict text =
    6.38 +fun read_const ctxt strict ty text =
    6.39    let val (c, pos) = token_content text in
    6.40      (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
    6.41        (SOME x, false) =>
    6.42          (Position.report (Markup.name x
    6.43              (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
    6.44 -          Free (x, infer_type ctxt x))
    6.45 +          Free (x, infer_type ctxt (x, ty)))
    6.46      | _ => prep_const_proper ctxt strict (c, pos))
    6.47    end;
    6.48  

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