src/Pure/Isar/locale.ML
changeset 30755 7ef503d216c2
parent 30754 c896167de3d5
child 30761 ac7570d80c3d
     1.1 --- a/src/Pure/Isar/locale.ML	Sat Mar 28 12:48:31 2009 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Sat Mar 28 16:00:54 2009 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4  sig
     1.5    (* Locale specification *)
     1.6    val register_locale: binding ->
     1.7 -    (string * sort) list * (binding * typ option * mixfix) list ->
     1.8 +    (string * sort) list * ((string * typ) * mixfix) list ->
     1.9      term option * term list ->
    1.10      thm option * thm option -> thm list ->
    1.11      declaration list * declaration list ->
    1.12 @@ -39,7 +39,7 @@
    1.13    val intern: theory -> xstring -> string
    1.14    val extern: theory -> string -> xstring
    1.15    val defined: theory -> string -> bool
    1.16 -  val params_of: theory -> string -> (binding * typ option * mixfix) list
    1.17 +  val params_of: theory -> string -> ((string * typ) * mixfix) list
    1.18    val intros_of: theory -> string -> thm option * thm option
    1.19    val axioms_of: theory -> string -> thm list
    1.20    val instance_of: theory -> string -> morphism -> term list
    1.21 @@ -91,7 +91,7 @@
    1.22  
    1.23  datatype locale = Loc of {
    1.24    (** static part **)
    1.25 -  parameters: (string * sort) list * (binding * typ option * mixfix) list,
    1.26 +  parameters: (string * sort) list * ((string * typ) * mixfix) list,
    1.27      (* type and term parameters *)
    1.28    spec: term option * term list,
    1.29      (* assumptions (as a single predicate expression) and defines *)
    1.30 @@ -165,7 +165,7 @@
    1.31  fun axioms_of thy = #axioms o the_locale thy;
    1.32  
    1.33  fun instance_of thy name morph = params_of thy name |>
    1.34 -  map (fn (b, T, _) => Morphism.term morph (Free (Name.of_binding b, the T)));
    1.35 +  map (Morphism.term morph o Free o #1);
    1.36  
    1.37  fun specification_of thy = #spec o the_locale thy;
    1.38  
    1.39 @@ -285,7 +285,8 @@
    1.40        the_locale thy name;
    1.41    in
    1.42      input |>
    1.43 -      (if not (null params) then activ_elem (Fixes params) else I) |>
    1.44 +      (not (null params) ?
    1.45 +        activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
    1.46        (* FIXME type parameters *)
    1.47        (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
    1.48        (if not (null defs)