# HG changeset patch
# User wenzelm
# Date 1333296079 -7200
# Node ID 23654b331d5cefa7ceb191ff05e686b6994c1a39
# Parent  2bbab021c0e6c8e5b8a0d378dbeac8a7b8960bb4
tuned signature;

diff -r 2bbab021c0e6 -r 23654b331d5c src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Apr 01 15:23:43 2012 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sun Apr 01 18:01:19 2012 +0200
@@ -248,13 +248,13 @@
 fun type_notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args in
     declaration {syntax = true, pervasive = false}
-      (Proof_Context.target_type_notation add mode args) lthy
+      (Proof_Context.generic_type_notation add mode args) lthy
   end;
 
 fun notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args in
     declaration {syntax = true, pervasive = false}
-      (Proof_Context.target_notation add mode args) lthy
+      (Proof_Context.generic_notation add mode args) lthy
   end;
 
 
diff -r 2bbab021c0e6 -r 23654b331d5c src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun Apr 01 15:23:43 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Sun Apr 01 18:01:19 2012 +0200
@@ -75,7 +75,7 @@
             same_shape ?
               (Context.mapping
                 (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
-               Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
+               Morphism.form (Proof_Context.generic_notation true prmode [(lhs', mx)]))))
     end);
 
 
diff -r 2bbab021c0e6 -r 23654b331d5c src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Apr 01 15:23:43 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Apr 01 18:01:19 2012 +0200
@@ -136,9 +136,9 @@
   val get_case: Proof.context -> string -> binding option list -> Rule_Cases.T
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
-  val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
+  val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
     Context.generic -> Context.generic
-  val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
+  val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
   val class_alias: binding -> class -> Proof.context -> Proof.context
   val type_alias: binding -> string -> Proof.context -> Proof.context
@@ -970,7 +970,7 @@
 val type_notation = gen_notation (K type_syntax);
 val notation = gen_notation const_syntax;
 
-fun target_type_notation add mode args phi =
+fun generic_type_notation add mode args phi =
   let
     val args' = args |> map_filter (fn (T, mx) =>
       let
@@ -979,7 +979,7 @@
       in if similar then SOME (T', mx) else NONE end);
   in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end;
 
-fun target_notation add mode args phi =
+fun generic_notation add mode args phi =
   let
     val args' = args |> map_filter (fn (t, mx) =>
       let val t' = Morphism.term phi t