--- a/src/Pure/Thy/export_theory.ML Mon Dec 02 16:28:23 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML Tue Dec 03 10:50:28 2019 +0100
@@ -120,25 +120,6 @@
in SOME (dep, (substT, subst)) end);
-(* spec rules *)
-
-fun spec_rule_content {pos, name, rough_classification, terms, rules} =
- let
- val spec =
- terms @ map Thm.plain_prop_of rules
- |> Term_Subst.zero_var_indexes_list
- |> map Logic.unvarify_global;
- in
- {props = Position.properties_of pos,
- name = name,
- rough_classification = rough_classification,
- typargs = rev (fold Term.add_tfrees spec []),
- args = rev (fold Term.add_frees spec []),
- terms = map (fn t => (t, Term.type_of t)) (take (length terms) spec),
- rules = drop (length terms) spec}
- end;
-
-
(* general setup *)
fun setup_presentation f =
@@ -160,14 +141,32 @@
val thy_ctxt = Proof_Context.init_global thy;
+ (* spec rules *)
+
+ fun position_properties pos =
+ Position.offset_properties_of (adjust_pos pos) @ Position.id_properties_of pos;
+
+ fun spec_rule_content {pos, name, rough_classification, terms, rules} =
+ let
+ val spec =
+ terms @ map Thm.plain_prop_of rules
+ |> Term_Subst.zero_var_indexes_list
+ |> map Logic.unvarify_global;
+ in
+ {props = position_properties pos,
+ name = name,
+ rough_classification = rough_classification,
+ typargs = rev (fold Term.add_tfrees spec []),
+ args = rev (fold Term.add_frees spec []),
+ terms = map (fn t => (t, Term.type_of t)) (take (length terms) spec),
+ rules = drop (length terms) spec}
+ end;
+
+
(* entities *)
fun make_entity_markup name xname pos serial =
- let
- val props =
- Position.offset_properties_of (adjust_pos pos) @
- Position.id_properties_of pos @
- Markup.serial_properties serial;
+ let val props = position_properties pos @ Markup.serial_properties serial;
in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
fun entity_markup space name =