529 |
529 |
530 (*Simplify both terms and check for assignments. |
530 (*Simplify both terms and check for assignments. |
531 Bound vars in the binder are "banned" unless used in both t AND u *) |
531 Bound vars in the binder are "banned" unless used in both t AND u *) |
532 fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) = |
532 fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) = |
533 let val loot = loose_bnos t and loou = loose_bnos u |
533 let val loot = loose_bnos t and loou = loose_bnos u |
534 fun add_index (((a,T), j), (bnos, newbinder)) = |
534 fun add_index (j, (a,T)) (bnos, newbinder) = |
535 if member (op =) loot j andalso member (op =) loou j |
535 if member (op =) loot j andalso member (op =) loou j |
536 then (bnos, (a,T)::newbinder) (*needed by both: keep*) |
536 then (bnos, (a,T)::newbinder) (*needed by both: keep*) |
537 else (j::bnos, newbinder); (*remove*) |
537 else (j::bnos, newbinder); (*remove*) |
538 val indices = 0 upto (length rbinder - 1); |
538 val (banned,rbin') = fold_rev add_index |
539 val (banned,rbin') = List.foldr add_index ([],[]) (rbinder~~indices); |
539 ((0 upto (length rbinder - 1)) ~~ rbinder) ([],[]); |
540 val (env', t') = clean_term banned (env, t); |
540 val (env', t') = clean_term banned (env, t); |
541 val (env'',u') = clean_term banned (env',u) |
541 val (env'',u') = clean_term banned (env',u) |
542 in (ff_assign thy (env'', rbin', t', u'), tpairs) |
542 in (ff_assign thy (env'', rbin', t', u'), tpairs) |
543 handle ASSIGN => (ff_assign thy (env'', rbin', u', t'), tpairs) |
543 handle ASSIGN => (ff_assign thy (env'', rbin', u', t'), tpairs) |
544 handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs)) |
544 handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs)) |