298 val rew_ss = HOL_basic_ss addsimps all_f_defs |
298 val rew_ss = HOL_basic_ss addsimps all_f_defs |
299 val mpsimps = map2 mk_mpsimp fqgars psimps |
299 val mpsimps = map2 mk_mpsimp fqgars psimps |
300 val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
300 val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
301 val mtermination = full_simplify rew_ss termination |
301 val mtermination = full_simplify rew_ss termination |
302 val mdomintros = Option.map (map (full_simplify rew_ss)) domintros |
302 val mdomintros = Option.map (map (full_simplify rew_ss)) domintros |
303 val meqvts = mk_meqvts lthy eqvt all_f_defs |
303 val meqvts = [eqvt] (*mk_meqvts lthy eqvt all_f_defs*) |
304 in |
304 in |
305 NominalFunctionResult { fs=fs, G=G, R=R, |
305 NominalFunctionResult { fs=fs, G=G, R=R, |
306 psimps=mpsimps, simple_pinducts=minducts, |
306 psimps=mpsimps, simple_pinducts=minducts, |
307 cases=cases, termination=mtermination, |
307 cases=cases, termination=mtermination, |
308 domintros=mdomintros, eqvts=meqvts } |
308 domintros=mdomintros, eqvts=meqvts } |