src/Pure/sign.ML
changeset 20155 da0505518e69
parent 19806 f860b7a98445
child 20211 c7f907f41f7c
     1.1 --- a/src/Pure/sign.ML	Wed Jul 19 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Jul 19 12:11:57 2006 +0200
     1.3 @@ -177,14 +177,14 @@
     1.4    val read_tyname: theory -> string -> typ
     1.5    val read_const: theory -> string -> term
     1.6    val infer_types_simult: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
     1.7 -    (indexname -> sort option) -> string list -> bool
     1.8 +    (indexname -> sort option) -> Name.context -> bool
     1.9      -> (term list * typ) list -> term list * (indexname * typ) list
    1.10    val infer_types: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
    1.11 -    (indexname -> sort option) -> string list -> bool
    1.12 +    (indexname -> sort option) -> Name.context -> bool
    1.13      -> term list * typ -> term * (indexname * typ) list
    1.14    val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T ->
    1.15      Context.generic -> (indexname -> typ option) * (indexname -> sort option) ->
    1.16 -    string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
    1.17 +    Name.context -> bool -> (string * typ) list -> term list * (indexname * typ) list
    1.18    val read_def_terms:
    1.19      theory * (indexname -> typ option) * (indexname -> sort option) ->
    1.20      string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
    1.21 @@ -574,7 +574,7 @@
    1.22  (*
    1.23    def_type: partial map from indexnames to types (constrains Frees and Vars)
    1.24    def_sort: partial map from indexnames to sorts (constrains TFrees and TVars)
    1.25 -  used: list of already used type variables
    1.26 +  used: context of already used type variables
    1.27    freeze: if true then generated parameters are turned into TFrees, else TVars
    1.28  
    1.29    termss: lists of alternative parses (only one combination should be type-correct)
    1.30 @@ -627,9 +627,9 @@
    1.31        in (Syntax.read context is_logtype syn T' s, T') end;
    1.32    in infer_types_simult pp thy consts types sorts used freeze (map read sTs) end;
    1.33  
    1.34 -fun read_def_terms (thy, types, sorts) =
    1.35 +fun read_def_terms (thy, types, sorts) used =
    1.36    read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (consts_of thy)
    1.37 -    (Context.Theory thy) (types, sorts);
    1.38 +    (Context.Theory thy) (types, sorts) (Name.make_context used);
    1.39  
    1.40  fun simple_read_term thy T s =
    1.41    let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]