src/Pure/Isar/specification.ML

     local_theory -> (term * (bstring * thm)) list * local_theory
   val abbreviation: Syntax.mode -> ((string * string option * mixfix) option * string) list ->
     local_theory -> local_theory
   val abbreviation_i: Syntax.mode -> ((string * typ option * mixfix) option * term) list ->
     local_theory -> local_theory
-  val const_syntax: Syntax.mode -> (xstring * mixfix) list -> local_theory -> local_theory
-  val const_syntax_i: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
+  val notation: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
+  val notation_i: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val theorems: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
     -> local_theory -> (bstring * thm list) list * local_theory
   val theorems_i: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
     -> local_theory -> (bstring * thm list) list * local_theory
   val theorem: string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->

 val abbreviation_i = gen_abbrevs cert_specification;
 
 
 (* const syntax *)
 
-fun gen_syntax intern_const mode raw_args lthy =
-  let val args = raw_args |> map (apfst (intern_const (ProofContext.consts_of lthy)))
-  in lthy |> LocalTheory.const_syntax mode args end;
-
-val const_syntax = gen_syntax Consts.intern;
-val const_syntax_i = gen_syntax (K I);
+fun gen_notation prep_const mode args lthy =
+  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
+
+val notation = gen_notation ProofContext.read_const;
+val notation_i = gen_notation (K I);
 
 
 (* fact statements *)
 
 fun gen_theorems prep_thms prep_att kind raw_facts lthy =

 fun gen_theorem prep_att prep_stmt
     kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 =
   let
     val _ = LocalTheory.assert lthy0;
     val thy = ProofContext.theory_of lthy0;
-    
+
     val (loc, ctxt, lthy) =
       (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
         (SOME loc, true) => (* workaround non-modularity of in/includes *)  (* FIXME *)
           (warning "Re-initializing theory target for locale inclusion";
             (SOME loc, ProofContext.init thy, LocalTheory.reinit lthy0))