# HG changeset patch
# User wenzelm
# Date 1213905901 -7200
# Node ID 2ddb6a2db65c94636c77b53e43fe0b450790dfbe
# Parent  ebd0291ea79c2592b0fabc8ee839cd8d288c8c88
moved get_sort to Isar/proof_context.ML;
removed obsolete read_def_typ, read_typ, read_typ_syntax, read_typ_abbrev;

diff -r ebd0291ea79c -r 2ddb6a2db65c src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Jun 19 21:14:30 2008 +0200
+++ b/src/Pure/sign.ML	Thu Jun 19 22:05:01 2008 +0200
@@ -78,12 +78,6 @@
   val read_class: theory -> xstring -> class
   val read_arity: theory -> xstring * string list * string -> arity
   val cert_arity: theory -> arity -> arity
-  val get_sort: theory ->
-    (indexname -> sort option) -> (indexname * sort) list -> indexname -> sort
-  val read_def_typ: theory * (indexname -> sort option) -> string -> typ
-  val read_typ: theory -> string -> typ
-  val read_typ_syntax: theory -> string -> typ
-  val read_typ_abbrev: theory -> string -> typ
   val add_defsort: string -> theory -> theory
   val add_defsort_i: sort -> theory -> theory
   val add_types: (bstring * int * mixfix) list -> theory -> theory
@@ -427,53 +421,6 @@
 val cert_arity = prep_arity (K I) certify_sort;
 
 
-(* types *)
-
-fun get_sort thy def_sort raw_env =
-  let
-    val tsig = tsig_of thy;
-
-    fun eq ((xi, S), (xi', S')) =
-      Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
-    val env = distinct eq raw_env;
-    val _ = (case duplicates (eq_fst (op =)) env of [] => ()
-      | dups => error ("Inconsistent sort constraints for type variable(s) "
-          ^ commas_quote (map (Term.string_of_vname' o fst) dups)));
-
-    fun get xi =
-      (case (AList.lookup (op =) env xi, def_sort xi) of
-        (NONE, NONE) => Type.defaultS tsig
-      | (NONE, SOME S) => S
-      | (SOME S, NONE) => S
-      | (SOME S, SOME S') =>
-          if Type.eq_sort tsig (S, S') then S'
-          else error ("Sort constraint inconsistent with default for type variable " ^
-            quote (Term.string_of_vname' xi)));
-  in get end;
-
-local
-
-fun gen_read_typ mode (thy, def_sort) str =
-  let
-    val ctxt = ProofContext.init thy;
-    val syn = syn_of thy;
-    val T = intern_tycons thy
-      (Syntax.standard_parse_typ ctxt syn (get_sort thy def_sort) (intern_sort thy) str);
-  in certify_typ_mode mode thy T handle TYPE (msg, _, _) => error msg end
-  handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
-
-in
-
-fun no_def_sort thy = (thy: theory, K NONE);
-
-val read_def_typ     = gen_read_typ Type.mode_default;
-val read_typ         = gen_read_typ Type.mode_default o no_def_sort;
-val read_typ_syntax  = gen_read_typ Type.mode_syntax o no_def_sort;
-val read_typ_abbrev  = gen_read_typ Type.mode_abbrev o no_def_sort;
-
-end;
-
-
 
 (** signature extension functions **)  (*exception ERROR/TYPE*)