src/Pure/sign.ML
changeset 27284 2ddb6a2db65c
parent 27257 ddc00dbad26b
child 27302 8d12ac6a3e1c
     1.1 --- a/src/Pure/sign.ML	Thu Jun 19 21:14:30 2008 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Jun 19 22:05:01 2008 +0200
     1.3 @@ -78,12 +78,6 @@
     1.4    val read_class: theory -> xstring -> class
     1.5    val read_arity: theory -> xstring * string list * string -> arity
     1.6    val cert_arity: theory -> arity -> arity
     1.7 -  val get_sort: theory ->
     1.8 -    (indexname -> sort option) -> (indexname * sort) list -> indexname -> sort
     1.9 -  val read_def_typ: theory * (indexname -> sort option) -> string -> typ
    1.10 -  val read_typ: theory -> string -> typ
    1.11 -  val read_typ_syntax: theory -> string -> typ
    1.12 -  val read_typ_abbrev: theory -> string -> typ
    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 @@ -427,53 +421,6 @@
    1.17  val cert_arity = prep_arity (K I) certify_sort;
    1.18  
    1.19  
    1.20 -(* types *)
    1.21 -
    1.22 -fun get_sort thy def_sort raw_env =
    1.23 -  let
    1.24 -    val tsig = tsig_of thy;
    1.25 -
    1.26 -    fun eq ((xi, S), (xi', S')) =
    1.27 -      Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
    1.28 -    val env = distinct eq raw_env;
    1.29 -    val _ = (case duplicates (eq_fst (op =)) env of [] => ()
    1.30 -      | dups => error ("Inconsistent sort constraints for type variable(s) "
    1.31 -          ^ commas_quote (map (Term.string_of_vname' o fst) dups)));
    1.32 -
    1.33 -    fun get xi =
    1.34 -      (case (AList.lookup (op =) env xi, def_sort xi) of
    1.35 -        (NONE, NONE) => Type.defaultS tsig
    1.36 -      | (NONE, SOME S) => S
    1.37 -      | (SOME S, NONE) => S
    1.38 -      | (SOME S, SOME S') =>
    1.39 -          if Type.eq_sort tsig (S, S') then S'
    1.40 -          else error ("Sort constraint inconsistent with default for type variable " ^
    1.41 -            quote (Term.string_of_vname' xi)));
    1.42 -  in get end;
    1.43 -
    1.44 -local
    1.45 -
    1.46 -fun gen_read_typ mode (thy, def_sort) str =
    1.47 -  let
    1.48 -    val ctxt = ProofContext.init thy;
    1.49 -    val syn = syn_of thy;
    1.50 -    val T = intern_tycons thy
    1.51 -      (Syntax.standard_parse_typ ctxt syn (get_sort thy def_sort) (intern_sort thy) str);
    1.52 -  in certify_typ_mode mode thy T handle TYPE (msg, _, _) => error msg end
    1.53 -  handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
    1.54 -
    1.55 -in
    1.56 -
    1.57 -fun no_def_sort thy = (thy: theory, K NONE);
    1.58 -
    1.59 -val read_def_typ     = gen_read_typ Type.mode_default;
    1.60 -val read_typ         = gen_read_typ Type.mode_default o no_def_sort;
    1.61 -val read_typ_syntax  = gen_read_typ Type.mode_syntax o no_def_sort;
    1.62 -val read_typ_abbrev  = gen_read_typ Type.mode_abbrev o no_def_sort;
    1.63 -
    1.64 -end;
    1.65 -
    1.66 -
    1.67  
    1.68  (** signature extension functions **)  (*exception ERROR/TYPE*)
    1.69