--- 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;
--- 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);
--- 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