--- a/src/Pure/Isar/generic_target.ML Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML Mon Jun 01 18:59:20 2015 +0200
@@ -7,17 +7,17 @@
signature GENERIC_TARGET =
sig
- (*consts*)
- val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
- local_theory -> local_theory
-
- (*background operations*)
+ (*background primitives*)
val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory
val background_declaration: declaration -> local_theory -> local_theory
val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
- (*lifting primitives to local theory operations*)
+ (*nested local theories primitives*)
+ val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
+ local_theory -> local_theory
+
+ (*lifting target primitives to local theory operations*)
val define: (((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory) ->
bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
@@ -63,29 +63,6 @@
structure Generic_Target: GENERIC_TARGET =
struct
-(** notes **)
-
-fun standard_facts lthy ctxt =
- Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
-
-fun standard_notes pred kind facts lthy =
- Local_Theory.map_contexts (fn level => fn ctxt =>
- if pred (Local_Theory.level lthy, level)
- then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
- else ctxt) lthy;
-
-
-
-(** declarations **)
-
-fun standard_declaration pred decl lthy =
- Local_Theory.map_contexts (fn level => fn ctxt =>
- if pred (Local_Theory.level lthy, level)
- then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
- else ctxt) lthy;
-
-
-
(** consts **)
fun check_mixfix ctxt (b, extra_tfrees) mx =
@@ -139,9 +116,6 @@
end
else context;
-fun standard_const pred prmode ((b, mx), rhs) =
- standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
-
(** background primitives **)
@@ -174,7 +148,28 @@
-(** lifting primitive to local theory operations **)
+(** nested local theories primitives **)
+
+fun standard_facts lthy ctxt =
+ Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
+
+fun standard_notes pred kind facts lthy =
+ Local_Theory.map_contexts (fn level => fn ctxt =>
+ if pred (Local_Theory.level lthy, level)
+ then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
+ else ctxt) lthy;
+
+fun standard_declaration pred decl lthy =
+ Local_Theory.map_contexts (fn level => fn ctxt =>
+ if pred (Local_Theory.level lthy, level)
+ then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
+ else ctxt) lthy;
+
+fun standard_const pred prmode ((b, mx), rhs) =
+ standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
+
+
+(** lifting target primitives to local theory operations **)
(* define *)