clarified Type.the_decl;
authorwenzelm
Sat Apr 23 18:25:50 2011 +0200 (2011-04-23)
changeset 42468aea61c5f88c3
parent 42467 1f7e39bdf0f6
child 42469 daa93275880e
clarified Type.the_decl;
src/Pure/Isar/proof_context.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat Apr 23 18:09:27 2011 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Apr 23 18:25:50 2011 +0200
     1.3 @@ -483,7 +483,7 @@
     1.4      else
     1.5        let
     1.6          val d = intern_type ctxt c;
     1.7 -        val decl = Type.the_decl tsig d handle ERROR msg => error (msg ^ Position.str_of pos);
     1.8 +        val decl = Type.the_decl tsig (d, pos);
     1.9          fun err () = error ("Bad type name: " ^ quote d ^ Position.str_of pos);
    1.10          val args =
    1.11            (case decl of
     2.1 --- a/src/Pure/ML/ml_antiquote.ML	Sat Apr 23 18:09:27 2011 +0200
     2.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sat Apr 23 18:25:50 2011 +0200
     2.3 @@ -121,7 +121,7 @@
     2.4    >> (fn (ctxt, (s, pos)) =>
     2.5      let
     2.6        val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
     2.7 -      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) c;
     2.8 +      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
     2.9        val res =
    2.10          (case try check (c, decl) of
    2.11            SOME res => res
     3.1 --- a/src/Pure/type.ML	Sat Apr 23 18:09:27 2011 +0200
     3.2 +++ b/src/Pure/type.ML	Sat Apr 23 18:25:50 2011 +0200
     3.3 @@ -51,7 +51,7 @@
     3.4    val intern_type: tsig -> xstring -> string
     3.5    val extern_type: Proof.context -> tsig -> string -> xstring
     3.6    val is_logtype: tsig -> string -> bool
     3.7 -  val the_decl: tsig -> string -> decl
     3.8 +  val the_decl: tsig -> string * Position.T -> decl
     3.9    val cert_typ_mode: mode -> tsig -> typ -> typ
    3.10    val cert_typ: tsig -> typ -> typ
    3.11    val arity_number: tsig -> string -> int
    3.12 @@ -246,9 +246,9 @@
    3.13  
    3.14  fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
    3.15  
    3.16 -fun the_decl tsig c =
    3.17 +fun the_decl tsig (c, pos) =
    3.18    (case lookup_type tsig c of
    3.19 -    NONE => error (undecl_type c)
    3.20 +    NONE => error (undecl_type c ^ Position.str_of pos)
    3.21    | SOME decl => decl);
    3.22  
    3.23  
    3.24 @@ -277,7 +277,7 @@
    3.25              val Ts' = map cert Ts;
    3.26              fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
    3.27            in
    3.28 -            (case the_decl tsig c of
    3.29 +            (case the_decl tsig (c, Position.none) of
    3.30                LogicalType n => (nargs n; Type (c, Ts'))
    3.31              | Abbreviation (vs, U, syn) =>
    3.32                 (nargs (length vs);