src/Pure/display.ML
changeset 14990 582b655da757
parent 14876 477c414000f8
child 14996 2571227f3fcc
equal deleted inserted replaced
14989:5a5d076a9863 14990:582b655da757
   201             prt_typ_no_tvars T, Pretty.str " ::", Pretty.brk 1, prt_sort S];
   201             prt_typ_no_tvars T, Pretty.str " ::", Pretty.brk 1, prt_sort S];
   202 
   202 
   203     fun pretty_nonterminals ts = Pretty.block
   203     fun pretty_nonterminals ts = Pretty.block
   204       (Pretty.breaks (Pretty.str "syntactic types:" :: map Pretty.str ts));
   204       (Pretty.breaks (Pretty.str "syntactic types:" :: map Pretty.str ts));
   205 
   205 
   206     fun pretty_abbr (t, (vs, rhs)) = Pretty.block
   206     fun pretty_abbr (t, (vs, rhs, _)) = Pretty.block
   207       [prt_typ_no_tvars (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
   207       [prt_typ_no_tvars (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
   208         Pretty.str " =", Pretty.brk 1, prt_typ_no_tvars rhs];
   208         Pretty.str " =", Pretty.brk 1, prt_typ_no_tvars rhs];
   209 
   209 
   210     fun pretty_arities (t, ars) = map (prt_arity t) ars;
   210     fun pretty_arities (t, ars) = map (prt_arity t) ars;
   211 
   211