src/Pure/sign.ML
changeset 267 ab78019b8ec8
parent 266 3fe01df1a614
child 277 4abe17e92130
     1.1 --- a/src/Pure/sign.ML	Tue Feb 08 14:09:34 1994 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Feb 09 14:25:29 1994 +0100
     1.3 @@ -209,6 +209,11 @@
     1.4  
     1.5  fun extend sg name (classes, default, types, abbrs, arities, consts, opt_sext) =
     1.6    let
     1.7 +    fun read_abbr syn (c, vs, rhs_src) =
     1.8 +      (c, (map (rpair 0) vs, varifyT (Syntax.read_typ syn (K []) rhs_src)))
     1.9 +        handle ERROR => error ("The error(s) above occurred in the rhs " ^
    1.10 +          quote rhs_src ^ "\nof type abbreviation " ^ quote c);
    1.11 +
    1.12      (*reset TVar indices to 0, renaming to preserve distinctness*)
    1.13      fun zero_tvar_idxs T =
    1.14        let
    1.15 @@ -225,10 +230,6 @@
    1.16        (c, zero_tvar_idxs (varifyT (rd_typ tsig syn (K None) s)))
    1.17          handle ERROR => error ("in declaration of constant " ^ quote c);
    1.18  
    1.19 -    fun read_abbr tsig syn (c, vs, rhs_src) =
    1.20 -      (c, (map (rpair 0) vs, varifyT (rd_typ tsig syn (K None) rhs_src)
    1.21 -        handle ERROR => error ("in type abbreviation " ^ quote c)));
    1.22 -
    1.23  
    1.24      val Sg {tsig, const_tab, syn, stamps} = sg;
    1.25      val xconsts = map #1 classes @ flat (map #1 types) @ map #1 abbrs @
    1.26 @@ -236,7 +237,7 @@
    1.27      val sext = if_none opt_sext Syntax.empty_sext;
    1.28  
    1.29      val tsig' = extend_tsig tsig (classes, default, types, arities);
    1.30 -    val tsig1 = ext_tsig_abbrs tsig' (map (read_abbr tsig' syn) abbrs);
    1.31 +    val tsig1 = ext_tsig_abbrs tsig' (map (read_abbr syn) abbrs);
    1.32  
    1.33      val syn1 = Syntax.extend syn (rd_typ tsig1 syn (K None))
    1.34        (logical_types tsig1, xconsts, sext);