src/Pure/Isar/specification.ML
changeset 21206 2af4c7b3f7ef
parent 21036 0eed532acfca
child 21230 abfdce60b371
     1.1 --- a/src/Pure/Isar/specification.ML	Tue Nov 07 11:46:47 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Tue Nov 07 11:46:48 2006 +0100
     1.3 @@ -34,8 +34,8 @@
     1.4      local_theory -> local_theory
     1.5    val abbreviation_i: Syntax.mode -> ((string * typ option * mixfix) option * term) list ->
     1.6      local_theory -> local_theory
     1.7 -  val const_syntax: Syntax.mode -> (xstring * mixfix) list -> local_theory -> local_theory
     1.8 -  val const_syntax_i: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
     1.9 +  val notation: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    1.10 +  val notation_i: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.11    val theorems: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    1.12      -> local_theory -> (bstring * thm list) list * local_theory
    1.13    val theorems_i: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.14 @@ -174,12 +174,11 @@
    1.15  
    1.16  (* const syntax *)
    1.17  
    1.18 -fun gen_syntax intern_const mode raw_args lthy =
    1.19 -  let val args = raw_args |> map (apfst (intern_const (ProofContext.consts_of lthy)))
    1.20 -  in lthy |> LocalTheory.const_syntax mode args end;
    1.21 +fun gen_notation prep_const mode args lthy =
    1.22 +  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
    1.23  
    1.24 -val const_syntax = gen_syntax Consts.intern;
    1.25 -val const_syntax_i = gen_syntax (K I);
    1.26 +val notation = gen_notation ProofContext.read_const;
    1.27 +val notation_i = gen_notation (K I);
    1.28  
    1.29  
    1.30  (* fact statements *)
    1.31 @@ -220,7 +219,7 @@
    1.32    let
    1.33      val _ = LocalTheory.assert lthy0;
    1.34      val thy = ProofContext.theory_of lthy0;
    1.35 -    
    1.36 +
    1.37      val (loc, ctxt, lthy) =
    1.38        (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
    1.39          (SOME loc, true) => (* workaround non-modularity of in/includes *)  (* FIXME *)