# HG changeset patch
# User wenzelm
# Date 1165761042 -3600
# Node ID fe94c6797c0965fcccb66f68483b019aeafa1dad
# Parent  a330e58226d0a89f217093d84e16a57597de7c0c
added notation/abbrev (from term_syntax.ML);

diff -r a330e58226d0 -r fe94c6797c09 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Dec 10 15:30:40 2006 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sun Dec 10 15:30:42 2006 +0100
@@ -24,6 +24,7 @@
     ((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory
   val axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory ->
     (bstring * thm list) list * local_theory
+  val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> local_theory
   val defs: string -> ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list ->
     local_theory -> (term * (bstring * thm)) list * local_theory
   val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
@@ -35,6 +36,7 @@
     local_theory -> (term * (bstring * thm)) * local_theory
   val note: string -> (bstring * Attrib.src list) * thm list ->
     local_theory -> (bstring * thm list) * Proof.context
+  val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
   val target_name: local_theory -> bstring -> string
   val init: string -> operations -> Proof.context -> local_theory
@@ -56,6 +58,7 @@
     (term * thm) list * local_theory,
   axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory ->
     (bstring * thm list) list * local_theory,
+  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> local_theory,
   defs: string -> ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list ->
     local_theory -> (term * (bstring * thm)) list * local_theory,
   notes: string ->
@@ -153,6 +156,7 @@
 val pretty = operation #pretty;
 val consts = operation2 #consts;
 val axioms = operation2 #axioms;
+val abbrev = operation2 #abbrev;
 val defs = operation2 #defs;
 val notes = operation2 #notes;
 val type_syntax = operation1 #type_syntax;
@@ -164,6 +168,10 @@
 fun def kind arg lthy = lthy |> defs kind [arg] |>> hd;
 fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd;
 
+fun notation mode raw_args lthy =
+  let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
+  in term_syntax (ProofContext.target_notation mode args) lthy end;
+
 
 (* init -- exit *)