src/Pure/sign.ML
changeset 27257 ddc00dbad26b
parent 27205 56c96c02ab79
child 27284 2ddb6a2db65c
     1.1 --- a/src/Pure/sign.ML	Wed Jun 18 18:55:04 2008 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Jun 18 18:55:05 2008 +0200
     1.3 @@ -84,12 +84,6 @@
     1.4    val read_typ: theory -> string -> typ
     1.5    val read_typ_syntax: theory -> string -> typ
     1.6    val read_typ_abbrev: theory -> string -> typ
     1.7 -  val read_def_terms:
     1.8 -    theory * (indexname -> typ option) * (indexname -> sort option) ->
     1.9 -    string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
    1.10 -  val simple_read_term: theory -> typ -> string -> term
    1.11 -  val read_term: theory -> string -> term
    1.12 -  val read_prop: theory -> string -> term
    1.13    val add_defsort: string -> theory -> theory
    1.14    val add_defsort_i: sort -> theory -> theory
    1.15    val add_types: (bstring * int * mixfix) list -> theory -> theory
    1.16 @@ -480,58 +474,6 @@
    1.17  end;
    1.18  
    1.19  
    1.20 -(* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
    1.21 -
    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: context of already used type variables
    1.26 -  freeze: if true then generated parameters are turned into TFrees, else TVars
    1.27 -*)
    1.28 -
    1.29 -fun read_def_terms'
    1.30 -    pp is_logtype syn consts map_free ctxt (def_type, def_sort) used freeze raw_args =
    1.31 -  let
    1.32 -    val thy = ProofContext.theory_of ctxt;
    1.33 -    fun check_typs Ts = map (certify_typ thy) Ts
    1.34 -      handle TYPE (msg, _, _) => error msg;
    1.35 -
    1.36 -    fun infer args = TypeInfer.infer_types pp (tsig_of thy) check_typs
    1.37 -        (try (Consts.the_constraint consts)) def_type used ~1 (SOME freeze) args |>> map fst
    1.38 -      handle TYPE (msg, _, _) => error msg;
    1.39 -
    1.40 -    fun check T t = (singleton (fst o infer) (t, T); NONE) handle ERROR msg => SOME msg;
    1.41 -    fun map_const a = (true, #1 (Term.dest_Const (Consts.read_const consts a)))
    1.42 -      handle ERROR _ => (false, Consts.intern consts a);
    1.43 -    fun read T = Syntax.standard_parse_term pp (check T) (get_sort thy def_sort) map_const map_free
    1.44 -        (intern_tycons thy) (intern_sort thy) ctxt is_logtype syn T;
    1.45 -  in
    1.46 -    raw_args
    1.47 -    |> map (fn (s, raw_T) =>
    1.48 -      let val T = certify_typ thy raw_T handle TYPE (msg, _, _) => error msg
    1.49 -      in (read (#1 (TypeInfer.paramify_dummies T 0)) s, T) end)
    1.50 -    |> infer
    1.51 -  end;
    1.52 -
    1.53 -fun read_def_terms (thy, types, sorts) used freeze sTs =
    1.54 -  let
    1.55 -    val pp = Syntax.pp_global thy;
    1.56 -    val consts = consts_of thy;
    1.57 -    val cert_consts = Consts.certify pp (tsig_of thy) true consts;
    1.58 -    fun map_free x = if is_some (types (x, ~1)) then SOME x else NONE;
    1.59 -    val (ts, inst) =
    1.60 -      read_def_terms' pp (is_logtype thy) (syn_of thy) consts map_free
    1.61 -        (ProofContext.init thy) (types, sorts) (Name.make_context used) freeze sTs;
    1.62 -  in (map cert_consts ts, inst) end;
    1.63 -
    1.64 -fun simple_read_term thy T s =
    1.65 -  let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
    1.66 -  in t end handle ERROR msg => cat_error msg ("The error(s) above occurred for term " ^ s);
    1.67 -
    1.68 -fun read_term thy = simple_read_term thy dummyT;
    1.69 -fun read_prop thy = simple_read_term thy propT;
    1.70 -
    1.71 -
    1.72  
    1.73  (** signature extension functions **)  (*exception ERROR/TYPE*)
    1.74