equal
deleted
inserted
replaced
606 (Vect (k, R')) [js] = |
606 (Vect (k, R')) [js] = |
607 term_for_vect seen k R' T1 T2 T' js |
607 term_for_vect seen k R' T1 T2 T' js |
608 | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T' |
608 | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T' |
609 (Func (R1, Formula Neut)) jss = |
609 (Func (R1, Formula Neut)) jss = |
610 let |
610 let |
611 val _ = priority ("HERE: " ^ (if maybe_opt then "y" else "n")) (* ### *) |
|
612 val jss1 = all_combinations_for_rep R1 |
611 val jss1 = all_combinations_for_rep R1 |
613 val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1 |
612 val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1 |
614 val ts2 = |
613 val ts2 = |
615 map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0)) |
614 map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0)) |
616 [[int_from_bool (member (op =) jss js)]]) |
615 [[int_from_bool (member (op =) jss js)]]) |