src/Pure/Isar/specification.ML
changeset 24949 5f00e3532418
parent 24927 48e08f37ce92
child 24986 1f902ded7f70
     1.1 --- a/src/Pure/Isar/specification.ML	Wed Oct 10 17:31:55 2007 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Wed Oct 10 17:31:56 2007 +0200
     1.3 @@ -42,8 +42,8 @@
     1.4      local_theory -> local_theory
     1.5    val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string ->
     1.6      local_theory -> local_theory
     1.7 -  val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     1.8 -  val notation_cmd: 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 -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.12      -> local_theory -> (bstring * thm list) list * local_theory
    1.13    val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    1.14 @@ -221,8 +221,8 @@
    1.15  
    1.16  (* notation *)
    1.17  
    1.18 -fun gen_notation prep_const mode args lthy =
    1.19 -  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
    1.20 +fun gen_notation prep_const add mode args lthy =
    1.21 +  lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args);
    1.22  
    1.23  val notation = gen_notation (K I);
    1.24  val notation_cmd = gen_notation ProofContext.read_const;