equal
deleted
inserted
replaced
248 in |
248 in |
249 (Logic.list_all (params', prem), (rev vs, subst_bounds (vs, prem))) |
249 (Logic.list_all (params', prem), (rev vs, subst_bounds (vs, prem))) |
250 end) prems); |
250 end) prems); |
251 |
251 |
252 val ind_vars = |
252 val ind_vars = |
253 (Old_Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~ |
253 (Case_Translation.indexify_names (replicate (length atomTs) "pi") ~~ |
254 map NominalAtoms.mk_permT atomTs) @ [("z", fsT)]; |
254 map NominalAtoms.mk_permT atomTs) @ [("z", fsT)]; |
255 val ind_Ts = rev (map snd ind_vars); |
255 val ind_Ts = rev (map snd ind_vars); |
256 |
256 |
257 val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
257 val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
258 (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem, |
258 (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem, |