src/Pure/type.ML
changeset 12222 d1c276b45dbc
parent 11022 72a76580ed2f
child 12314 160013745a92
equal deleted inserted replaced
12221:cc31140bba16 12222:d1c276b45dbc
   530 
   530 
   531 fun ext_tsig_classes tsig new_classes =
   531 fun ext_tsig_classes tsig new_classes =
   532   let
   532   let
   533     val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
   533     val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
   534     val (classes', classrel') = extend_classes (classes,classrel, new_classes);
   534     val (classes', classrel') = extend_classes (classes,classrel, new_classes);
   535   in make_tsig (classes', classrel', default, tycons, log_types, univ_witness, abbrs, arities) end;
   535   in
       
   536     make_tsig (classes', classrel', default, tycons, log_types, univ_witness, abbrs, arities)
       
   537     |> rebuild_tsig
       
   538   end;
   536 
   539 
   537 
   540 
   538 (* ext_tsig_classrel *)
   541 (* ext_tsig_classrel *)
   539 
   542 
   540 fun ext_tsig_classrel tsig pairs =
   543 fun ext_tsig_classrel tsig pairs =