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