src/HOL/Tools/ATP/atp_translate.ML
changeset 43181 cd3b7798ecc2
parent 43179 db5fb1d4df42
child 43185 697d32fa183d
equal deleted inserted replaced
43180:283114859d6c 43181:cd3b7798ecc2
  1372   | fold_type_consts _ _ x = x
  1372   | fold_type_consts _ _ x = x
  1373 
  1373 
  1374 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
  1374 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
  1375 fun add_type_consts_in_term thy =
  1375 fun add_type_consts_in_term thy =
  1376   let
  1376   let
  1377     fun aux (Const (@{const_name Meson.skolem}, _) $ _) = I
  1377     fun add ((t as Const (s, _)) $ u) =
  1378       | aux (t $ u) = aux t #> aux u
  1378         if s = @{const_name Meson.skolem} orelse
  1379       | aux (Const x) =
  1379            String.isPrefix skolem_const_prefix s then
  1380         fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
  1380           I
  1381       | aux (Abs (_, _, u)) = aux u
  1381         else
  1382       | aux _ = I
  1382           add t #> add u
  1383   in aux end
  1383       | add (t $ u) = add t #> add u
       
  1384       | add (Const x) =
       
  1385         x |> Sign.const_typargs thy |> fold (fold_type_consts set_insert)
       
  1386       | add (Abs (_, _, u)) = add u
       
  1387       | add _ = I
       
  1388   in add end
  1384 
  1389 
  1385 fun type_consts_of_terms thy ts =
  1390 fun type_consts_of_terms thy ts =
  1386   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty)
  1391   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty)
  1387 
  1392 
  1388 fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
  1393 fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t