src/HOL/Tools/Metis/metis_translate.ML
changeset 43189 0ab7265f659f
parent 43180 283114859d6c
child 43190 494fde207706
equal deleted inserted replaced
43188:0c36ae874fcc 43189:0ab7265f659f
   286 
   286 
   287 fun type_ext thy tms =
   287 fun type_ext thy tms =
   288   let
   288   let
   289     val subs = tfree_classes_of_terms tms
   289     val subs = tfree_classes_of_terms tms
   290     val supers = tvar_classes_of_terms tms
   290     val supers = tvar_classes_of_terms tms
   291     val tycons = type_consts_of_terms thy tms
   291     val tycons = type_constrs_of_terms thy tms
   292     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   292     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   293     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   293     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   294   in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end
   294   in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end
   295 
   295 
   296 val proxy_defs = map (fst o snd o snd) proxy_table
   296 val proxy_defs = map (fst o snd o snd) proxy_table