# HG changeset patch
# User wenzelm
# Date 1165510730 -3600
# Node ID 785c3d0242c53a0cf625c170793d6005be58a6bf
# Parent  9395071cc5c5747ed518df1a689c977a5244a14f
moved notation/abbrevs to TermSyntax;

diff -r 9395071cc5c5 -r 785c3d0242c5 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Dec 07 17:58:50 2006 +0100
+++ b/src/Pure/Isar/local_theory.ML	Thu Dec 07 17:58:50 2006 +0100
@@ -35,8 +35,6 @@
     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 abbrevs: Syntax.mode -> ((bstring * mixfix) * term) 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
@@ -167,33 +165,6 @@
 fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd;
 
 
-(* term syntax *)
-
-fun generic_notation mode args phi =
-  let
-    val args' = args |> filter (fn (t, _) => t aconv Morphism.term phi t);
-  in Context.mapping (Sign.add_notation mode args') (ProofContext.add_notation mode args') end;
-
-fun notation mode args = term_syntax (generic_notation mode args);
-
-
-fun morph_abbrev phi ((c, mx), t) = ((Morphism.name phi c, mx), Morphism.term phi t);
-
-fun abbrevs mode raw_args lthy =
-  let val args = map (morph_abbrev (target_morphism lthy)) raw_args in
-    lthy |> term_syntax (fn phi =>
-      let
-        val args' = map (morph_abbrev phi) args;
-        val (abbrs, mxs) = (args ~~ args') |> map_filter (fn ((_, rhs), ((c', mx'), rhs')) =>
-            if rhs aconv rhs' then SOME (((c', NoSyn), rhs'), mx') else NONE)
-          |> split_list;
-      in
-        Context.mapping_result (Sign.add_abbrevs mode abbrs) (ProofContext.add_abbrevs mode abbrs)
-        #-> (fn res => generic_notation mode (map #1 res ~~ mxs) phi)
-      end)
-  end;
-
-
 (* init -- exit *)
 
 fun init theory_prefix operations target = target |> Data.map