1.1 --- a/src/Pure/Isar/specification.ML	Mon Mar 01 17:07:36 2010 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Mon Mar 01 17:09:42 2010 +0100
     1.3 @@ -42,6 +42,8 @@
     1.4      local_theory -> local_theory
     1.5    val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
     1.6      local_theory -> local_theory
     1.7 +  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
     1.8 +  val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
     1.9    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.10    val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    1.11    val theorems: string ->
    1.12 @@ -255,12 +257,24 @@
    1.13  
    1.14  (* notation *)
    1.15  
    1.16 +local
    1.17 +
    1.18 +fun gen_type_notation prep_type add mode args lthy =
    1.19 +  lthy |> Local_Theory.type_notation add mode (map (apfst (prep_type lthy)) args);
    1.20 +
    1.21  fun gen_notation prep_const add mode args lthy =
    1.22    lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
    1.23  
    1.24 +in
    1.25 +
    1.26 +val type_notation = gen_type_notation (K I);
    1.27 +val type_notation_cmd = gen_type_notation (fn ctxt => ProofContext.read_type_name ctxt false);
    1.28 +
    1.29  val notation = gen_notation (K I);
    1.30  val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false);
    1.31  
    1.32 +end;
    1.33 +
    1.34  
    1.35  (* fact statements *)
    1.36