equal
deleted
inserted
replaced
103 ~1 => Free ("", T) :: dist_vars Ts vs |
103 ~1 => Free ("", T) :: dist_vars Ts vs |
104 | i => (nth vs i) :: dist_vars Ts (del_index i vs) |
104 | i => (nth vs i) :: dist_vars Ts (del_index i vs) |
105 |
105 |
106 fun dest_case rebind t = |
106 fun dest_case rebind t = |
107 let |
107 let |
108 val (_ $ _ $ rhs :: _ $ _ $ match :: guards) = HOLogic.dest_conj t |
108 val ((_ $ _ $ rhs) :: (_ $ _ $ match) :: guards) = HOLogic.dest_conj t |
109 val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs |
109 val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs |
110 in |
110 in |
111 foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match] |
111 foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match] |
112 end |
112 end |
113 |
113 |