tuned;

--- a/src/Pure/Isar/expression.ML	Thu Aug 30 19:59:36 2018 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Aug 31 13:34:31 2018 +0200
@@ -531,12 +531,8 @@
 local
 
 fun props_of thy (name, morph) =
-  let
-    val (asm, defs) = Locale.specification_of thy name;
-  in
-    (case asm of NONE => defs | SOME asm => asm :: defs)
-    |> map (Morphism.term morph)
-  end;
+  let val (asm, defs) = Locale.specification_of thy name
+  in map (Morphism.term morph) (the_list asm @ defs) end;
 
 fun prep_goal_expression prep expression ctxt =
   let

--- a/src/Pure/Isar/locale.ML	Thu Aug 30 19:59:36 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Aug 31 13:34:31 2018 +0200
@@ -53,6 +53,7 @@
   val axioms_of: theory -> string -> thm list
   val instance_of: theory -> string -> morphism -> term list
   val specification_of: theory -> string -> term option * term list
+  val hyp_spec_of: theory -> string -> Element.context_i list
 
   (* Storing results *)
   val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
@@ -84,7 +85,6 @@
   val add_dependency: string -> registration -> theory -> theory
 
   (* Diagnostic *)
-  val hyp_spec_of: theory -> string -> Element.context_i list
   val print_locales: bool -> theory -> unit
   val print_locale: theory -> bool -> xstring * Position.T -> unit
   val print_registrations: Proof.context -> xstring * Position.T -> unit
@@ -220,8 +220,9 @@
 
 fun specification_of thy = #spec o the_locale thy;
 
-fun dependencies_of thy name = the_locale thy name |>
-  #dependencies;
+fun hyp_spec_of thy = #hyp_spec o the_locale thy;
+
+fun dependencies_of thy = #dependencies o the_locale thy;
 
 fun mixins_of thy name serial = the_locale thy name |>
   #mixins |> lookup_mixins serial;
@@ -693,8 +694,6 @@
 
 (*** diagnostic commands and interfaces ***)
 
-fun hyp_spec_of thy = #hyp_spec o the_locale thy;
-
 fun print_locales verbose thy =
   Pretty.block
     (Pretty.breaks