src/Pure/sign.ML

 
 (*errors are indicated by exception ERROR (with messages already printed)*)
 
 fun extend sg name (classes, default, types, abbrs, arities, consts, opt_sext) =
   let
+    fun read_abbr syn (c, vs, rhs_src) =
+      (c, (map (rpair 0) vs, varifyT (Syntax.read_typ syn (K []) rhs_src)))
+        handle ERROR => error ("The error(s) above occurred in the rhs " ^
+          quote rhs_src ^ "\nof type abbreviation " ^ quote c);
+
     (*reset TVar indices to 0, renaming to preserve distinctness*)
     fun zero_tvar_idxs T =
       let
         val inxSs = typ_tvars T;
         val nms' = variantlist (map (#1 o #1) inxSs, []);

       indices because type inference requires it*)
     fun read_const tsig syn (c, s) =
       (c, zero_tvar_idxs (varifyT (rd_typ tsig syn (K None) s)))
         handle ERROR => error ("in declaration of constant " ^ quote c);
 
-    fun read_abbr tsig syn (c, vs, rhs_src) =
-      (c, (map (rpair 0) vs, varifyT (rd_typ tsig syn (K None) rhs_src)
-        handle ERROR => error ("in type abbreviation " ^ quote c)));
-
 
     val Sg {tsig, const_tab, syn, stamps} = sg;
     val xconsts = map #1 classes @ flat (map #1 types) @ map #1 abbrs @
       flat (map #1 consts);
     val sext = if_none opt_sext Syntax.empty_sext;
 
     val tsig' = extend_tsig tsig (classes, default, types, arities);
-    val tsig1 = ext_tsig_abbrs tsig' (map (read_abbr tsig' syn) abbrs);
+    val tsig1 = ext_tsig_abbrs tsig' (map (read_abbr syn) abbrs);
 
     val syn1 = Syntax.extend syn (rd_typ tsig1 syn (K None))
       (logical_types tsig1, xconsts, sext);
 
     val all_consts = flat (map (fn (cs, s) => map (rpair s) cs)