src/Pure/Isar/specification.ML

     local_theory -> (term * (string * thm)) * local_theory
   val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option * term ->
     local_theory -> local_theory
   val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
     local_theory -> local_theory
+  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
+  val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val theorems: string ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory

 val abbreviation_cmd = gen_abbrev true read_free_spec;
 
 
 (* notation *)
 
+local
+
+fun gen_type_notation prep_type add mode args lthy =
+  lthy |> Local_Theory.type_notation add mode (map (apfst (prep_type lthy)) args);
+
 fun gen_notation prep_const add mode args lthy =
   lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
 
+in
+
+val type_notation = gen_type_notation (K I);
+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);
+
+end;
 
 
 (* fact statements *)
 
 fun gen_theorems prep_fact prep_att kind raw_facts lthy =