# HG changeset patch
# User wenzelm
# Date 1214057930 -7200
# Node ID 07754b7ba89d0ccd37f0fd686b8348b5364cca32
# Parent  2a884461a9f37f96fb3756c8f98ada6d4bf055d4
the_tags: explicit error message;
new_decl: Position.thread_data;

diff -r 2a884461a9f3 -r 07754b7ba89d src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Jun 21 16:18:49 2008 +0200
+++ b/src/Pure/type.ML	Sat Jun 21 16:18:50 2008 +0200
@@ -126,10 +126,6 @@
 val empty_tsig =
   build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table);
 
-fun lookup_type (TSig {types, ...}) = Option.map fst o Symtab.lookup (snd types);
-
-fun the_tags tsig = snd o the o lookup_type tsig;
-
 
 (* classes and sorts *)
 
@@ -167,10 +163,21 @@
 fun restore_mode ctxt = set_mode (get_mode ctxt);
 
 
+(* lookup types *)
+
+fun undecl_type c = "Undeclared type constructor: " ^ quote c;
+
+fun lookup_type (TSig {types, ...}) = Option.map fst o Symtab.lookup (snd types);
+
+fun the_tags tsig c =
+  (case lookup_type tsig c of
+    SOME (_, tags) => tags
+  | NONE => error (undecl_type c));
+
+
 (* certified types *)
 
 fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
-fun undecl_type c = "Undeclared type constructor: " ^ quote c;
 
 local
 
@@ -560,12 +567,13 @@
 
 fun new_decl naming tags (c, decl) (space, types) =
   let
+    val tags' = tags |> Position.default_properties (Position.thread_data ());
     val c' = NameSpace.full naming c;
     val space' = NameSpace.declare naming c' space;
     val types' =
       (case Symtab.lookup types c' of
         SOME ((decl', _), _) => err_in_decls c' decl decl'
-      | NONE => Symtab.update (c', ((decl, tags), serial ())) types);
+      | NONE => Symtab.update (c', ((decl, tags'), serial ())) types);
   in (space', types') end;
 
 fun the_decl (_, types) = fst o fst o the o Symtab.lookup types;