# HG changeset patch
# User wenzelm
# Date 1632218921 -7200
# Node ID 534b231ce0413779499bd13a92e0c8e6ebf79e5c
# Parent  9c1ad2f04660add6a8c016b3e0f03278f18c94ed
clarified modules;

diff -r 9c1ad2f04660 -r 534b231ce041 src/HOL/Library/code_lazy.ML
--- a/src/HOL/Library/code_lazy.ML	Tue Sep 21 11:34:58 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML	Tue Sep 21 12:08:41 2021 +0200
@@ -91,7 +91,7 @@
     val lthy' = (snd o Local_Theory.begin_nested) lthy
     val ((t, (_, thm)), lthy') = Specification.definition NONE [] [] 
       ((Thm.def_binding (Binding.name name), []), def) lthy'
-    val lthy' = Specification.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy'
+    val lthy' = Local_Theory.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy'
     val lthy = Local_Theory.end_nested lthy'
     val def_thm = singleton (Proof_Context.export lthy' lthy) thm
   in
diff -r 9c1ad2f04660 -r 534b231ce041 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Sep 21 11:34:58 2021 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue Sep 21 12:08:41 2021 +0200
@@ -65,7 +65,10 @@
   val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list ->
     local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
+  val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
+    local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
+  val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
   val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
@@ -319,9 +322,12 @@
 
 (* notation *)
 
-fun type_notation add mode raw_args lthy =
+local
+
+fun gen_type_notation prep_type add mode raw_args lthy =
   let
-    val args = map (apfst (Logic.type_map (Assumption.export_term lthy (target_of lthy)))) raw_args;
+    val prepare = prep_type lthy #> Logic.type_map (Assumption.export_term lthy (target_of lthy));
+    val args = map (apfst prepare) raw_args;
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.type_notation add mode args;
   in
@@ -329,9 +335,10 @@
       (Proof_Context.generic_type_notation add mode args') lthy
   end;
 
-fun notation add mode raw_args lthy =
+fun gen_notation prep_const add mode raw_args lthy =
   let
-    val args = map (apfst (Assumption.export_term lthy (target_of lthy))) raw_args
+    val prepare = prep_const lthy #> Assumption.export_term lthy (target_of lthy);
+    val args = map (apfst prepare) raw_args;
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.notation add mode args;
   in
@@ -339,6 +346,17 @@
       (Proof_Context.generic_notation add mode args') lthy
   end;
 
+in
+
+val type_notation = gen_type_notation (K I);
+val type_notation_cmd =
+  gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false});
+
+val notation = gen_notation (K I);
+val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false});
+
+end;
+
 
 (* name space aliases *)
 
diff -r 9c1ad2f04660 -r 534b231ce041 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Sep 21 11:34:58 2021 +0200
+++ b/src/Pure/Isar/specification.ML	Tue Sep 21 12:08:41 2021 +0200
@@ -46,11 +46,6 @@
   val alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory
   val type_alias: binding * string -> local_theory -> local_theory
   val type_alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory
-  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
-  val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
-    local_theory -> local_theory
-  val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
-  val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val theorems: string ->
     (Attrib.binding * Attrib.thms) list ->
     (binding * typ option * mixfix) list ->
@@ -334,28 +329,6 @@
   gen_alias Local_Theory.type_alias (apfst (#1 o dest_Type) ooo Proof_Context.check_type_name);
 
 
-(* notation *)
-
-local
-
-fun gen_type_notation prep_type add mode args lthy =
-  lthy |> Local_Theory.type_notation add mode (map (apfst (prep_type lthy)) args);
-
-fun gen_notation prep_const add mode args lthy =
-  lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
-
-in
-
-val type_notation = gen_type_notation (K I);
-val type_notation_cmd =
-  gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false});
-
-val notation = gen_notation (K I);
-val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false});
-
-end;
-
-
 (* fact statements *)
 
 local
diff -r 9c1ad2f04660 -r 534b231ce041 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Sep 21 11:34:58 2021 +0200
+++ b/src/Pure/Pure.thy	Tue Sep 21 12:08:41 2021 +0200
@@ -499,25 +499,25 @@
   Outer_Syntax.local_theory \<^command_keyword>\<open>type_notation\<close>
     "add concrete syntax for type constructors"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
+      >> (fn (mode, args) => Local_Theory.type_notation_cmd true mode args));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>no_type_notation\<close>
     "delete concrete syntax for type constructors"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
+      >> (fn (mode, args) => Local_Theory.type_notation_cmd false mode args));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>notation\<close>
     "add concrete syntax for constants / fixed variables"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.notation_cmd true mode args));
+      >> (fn (mode, args) => Local_Theory.notation_cmd true mode args));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>no_notation\<close>
     "delete concrete syntax for constants / fixed variables"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.notation_cmd false mode args));
+      >> (fn (mode, args) => Local_Theory.notation_cmd false mode args));
 
 in end\<close>