383 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
383 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
384 val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 induct); |
384 val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 induct); |
385 fun note_simp_suffix s th ctxt = |
385 fun note_simp_suffix s th ctxt = |
386 snd (Local_Theory.note ((Binding.name (q_name ^ "_" ^ s), |
386 snd (Local_Theory.note ((Binding.name (q_name ^ "_" ^ s), |
387 [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
387 [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
388 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; |
388 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), |
|
389 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; |
389 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
390 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
390 val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14; |
391 val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14; |
391 val q_perm = map (lift_thm lthy14) raw_perm_def; |
392 val q_perm = map (lift_thm lthy14) raw_perm_def; |
392 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
393 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
393 val q_fv = map (lift_thm lthy15) fv_def; |
394 val q_fv = map (lift_thm lthy15) fv_def; |