202 in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end; |
202 in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end; |
203 |
203 |
204 fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies = |
204 fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies = |
205 let |
205 let |
206 val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); |
206 val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); |
207 val premss = List.mapPartial (fn (s, rs) => if s mem rsets then |
207 val premss = map_filter (fn (s, rs) => if member (op =) rsets s then |
208 SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct, |
208 SOME (rs, map (fn (_, r) => nth (prems_of raw_induct) |
209 find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss; |
209 (find_index (fn prp => prp = prop_of r) (map prop_of intrs))) rs) else NONE) rss; |
210 val fs = maps (fn ((intrs, prems), dummy) => |
210 val fs = maps (fn ((intrs, prems), dummy) => |
211 let |
211 let |
212 val fs = map (fn (rule, (ivs, intr)) => |
212 val fs = map (fn (rule, (ivs, intr)) => |
213 fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs) |
213 fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs) |
214 in if dummy then Const ("HOL.default_class.default", |
214 in if dummy then Const ("HOL.default_class.default", |