src/Pure/Isar/proof_context.ML
changeset 14257 a7ef3f7588c5
parent 14174 f3cafd2929d5
child 14287 f630017ed01c
equal deleted inserted replaced
14256:33e5ef9a4c98 14257:a7ef3f7588c5
    27   val read_typ_no_norm: context -> string -> typ
    27   val read_typ_no_norm: context -> string -> typ
    28   val cert_typ: context -> typ -> typ
    28   val cert_typ: context -> typ -> typ
    29   val cert_typ_no_norm: context -> typ -> typ
    29   val cert_typ_no_norm: context -> typ -> typ
    30   val get_skolem: context -> string -> string
    30   val get_skolem: context -> string -> string
    31   val extern_skolem: context -> term -> term
    31   val extern_skolem: context -> term -> term
    32   val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
    32   val read_termTs: string list -> context -> (string * typ) list -> term list * (indexname * typ) list
    33   val read_termTs_env: (indexname -> typ option) * (indexname -> sort option) * string list -> context -> (string * typ) list -> term list * (indexname * typ) list
    33   val read_termTs_env: (indexname -> typ option) * (indexname -> sort option) * string list -> context -> (string * typ) list -> term list * (indexname * typ) list
    34   val read_term: context -> string -> term
    34   val read_term: context -> string -> term
    35   val read_prop: context -> string -> term
    35   val read_prop: context -> string -> term
    36   val read_prop_schematic: context -> string -> term
    36   val read_prop_schematic: context -> string -> term
    37   val read_terms: context -> string list -> term list
    37   val read_terms: context -> string list -> term list
   589     |> app (if is_pat then prepare_dummies
   589     |> app (if is_pat then prepare_dummies
   590 	 else if dummies then I else reject_dummies ctxt)
   590 	 else if dummies then I else reject_dummies ctxt)
   591   end
   591   end
   592 in
   592 in
   593 
   593 
   594 val read_termTs =
   594 (* For where attribute:
   595   gen_read (read_def_termTs false) (apfst o map) None false false false false;
   595    Type vars generated by read will be distinct from those in "used". *)
       
   596 fun read_termTs used =
       
   597   gen_read (read_def_termTs false) (apfst o map) (Some (K None, K None, used)) false false false false;
   596 (* For rule_tac:
   598 (* For rule_tac:
   597    takes extra environment (types, sorts and used type vars) *)
   599    takes extra environment (types, sorts and used type vars) *)
   598 fun read_termTs_env env =
   600 fun read_termTs_env env =
   599   gen_read (read_def_termTs false) (apfst o map) (Some env) true false false false;
   601   gen_read (read_def_termTs false) (apfst o map) (Some env) true false false false;
   600 val read_termT_pats =
   602 val read_termT_pats =