src/HOL/Tools/ATP/atp_translate.ML
changeset 43121 5df3777f376d
parent 43120 a9c2cdf4ae97
child 43125 ddf63baabdec
equal deleted inserted replaced
43120:a9c2cdf4ae97 43121:5df3777f376d
  1330 
  1330 
  1331 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
  1331 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
  1332 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
  1332 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
  1333 
  1333 
  1334 fun classes_of_terms get_Ts =
  1334 fun classes_of_terms get_Ts =
  1335   map (map #2 o get_Ts)
  1335   map (map snd o get_Ts)
  1336   #> List.foldl add_classes Symtab.empty
  1336   #> List.foldl add_classes Symtab.empty
  1337   #> delete_type #> Symtab.keys
  1337   #> delete_type #> Symtab.keys
  1338 
  1338 
  1339 val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
  1339 val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
  1340 val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
  1340 val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars