src/Pure/Isar/locale.ML

 
 signature LOCALE =
 sig
   (* Locale specification *)
   val register_locale: binding ->
-    (string * sort) list * (binding * typ option * mixfix) list ->
+    (string * sort) list * ((string * typ) * mixfix) list ->
     term option * term list ->
     thm option * thm option -> thm list ->
     declaration list * declaration list ->
     (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
     (string * morphism) list -> theory -> theory
   val intern: theory -> xstring -> string
   val extern: theory -> string -> xstring
   val defined: theory -> string -> bool
-  val params_of: theory -> string -> (binding * typ option * mixfix) list
+  val params_of: theory -> string -> ((string * typ) * mixfix) list
   val intros_of: theory -> string -> thm option * thm option
   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 declarations_of: theory -> string -> declaration list * declaration list

 
 (*** Theory data ***)
 
 datatype locale = Loc of {
   (** static part **)
-  parameters: (string * sort) list * (binding * typ option * mixfix) list,
+  parameters: (string * sort) list * ((string * typ) * mixfix) list,
     (* type and term parameters *)
   spec: term option * term list,
     (* assumptions (as a single predicate expression) and defines *)
   intros: thm option * thm option,
   axioms: thm list,

 fun intros_of thy = #intros o the_locale thy;
 
 fun axioms_of thy = #axioms o the_locale thy;
 
 fun instance_of thy name morph = params_of thy name |>
-  map (fn (b, T, _) => Morphism.term morph (Free (Name.of_binding b, the T)));
+  map (Morphism.term morph o Free o #1);
 
 fun specification_of thy = #spec o the_locale thy;
 
 fun declarations_of thy name = the_locale thy name |>
   #decls |> pairself (map fst);

   let
     val {parameters = (_, params), spec = (asm, defs), ...} =
       the_locale thy name;
   in
     input |>
-      (if not (null params) then activ_elem (Fixes params) else I) |>
+      (not (null params) ?
+        activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
       (* FIXME type parameters *)
       (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
       (if not (null defs)
         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
         else I) |>