equal
deleted
inserted
replaced
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 |