equal
deleted
inserted
replaced
86 |
86 |
87 exception REIF of string; |
87 exception REIF of string; |
88 |
88 |
89 fun dest_listT (Type ("List.list", [T])) = T; |
89 fun dest_listT (Type ("List.list", [T])) = T; |
90 |
90 |
91 fun partition P [] = ([],[]) |
|
92 | partition P (x::xs) = |
|
93 let val (yes,no) = partition P xs |
|
94 in if P x then (x::yes,no) else (yes, x::no) end |
|
95 |
|
96 fun rearrange congs = |
91 fun rearrange congs = |
97 let |
92 let |
98 fun P (_, th) = |
93 fun P (_, th) = |
99 let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th |
94 let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th |
100 in can dest_Var l end |
95 in can dest_Var l end |
101 val (yes,no) = partition P congs |
96 val (yes,no) = List.partition P congs |
102 in no @ yes end |
97 in no @ yes end |
103 |
98 |
104 fun genreif ctxt raw_eqs t = |
99 fun genreif ctxt raw_eqs t = |
105 let |
100 let |
106 val bds = ref ([]: (typ * ((term list) * (term list))) list); |
101 val bds = ref ([]: (typ * ((term list) * (term list))) list); |