Lines Matching defs:tx
1275 val tL_simple = all (fn tx => is_var tx orelse
1276 let val (tx_b, tx_v) = dest_comb tx
1340 fun remove_free_var (n, tx) = is_comb tx andalso
1360 | mk_tL (sub,tL') ((n, tx)::ntL) =
1363 val (sub', tL'') = if not do_remove then (sub, tx::tL') else
1365 val (tx_b, tx_v) = dest_comb tx;
1366 val tx' = genvar (type_of tx);
1369 ((tx_b |-> mk_abs(tx_v, tx'))::sub, tx'::tL')
1375 val tL'' = map (fn tx => (true, fst (dest_comb tx)) handle HOL_ERR _ => (false, tx)) tL'