533 ((Binding.empty, [Rule_Cases.inner_rule, Induct.induct_type ""]), [([induct], [])])) |
533 ((Binding.empty, [Rule_Cases.inner_rule, Induct.induct_type ""]), [([induct], [])])) |
534 (drop (length dt_names) inducts); |
534 (drop (length dt_names) inducts); |
535 |
535 |
536 val ctxt = Proof_Context.init_global thy9; |
536 val ctxt = Proof_Context.init_global thy9; |
537 val case_combs = |
537 val case_combs = |
538 map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT) case_names; |
538 map (Proof_Context.read_const ctxt {proper = false, strict = false}) case_names; |
539 val constrss = map (fn (dtname, {descr, index, ...}) => |
539 val constrss = map (fn (dtname, {descr, index, ...}) => |
540 map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT o fst) |
540 map (Proof_Context.read_const ctxt {proper = false, strict = false} o fst) |
541 (#3 (the (AList.lookup op = descr index)))) dt_infos; |
541 (#3 (the (AList.lookup op = descr index)))) dt_infos; |
542 in |
542 in |
543 thy9 |
543 thy9 |
544 |> Global_Theory.note_thmss "" |
544 |> Global_Theory.note_thmss "" |
545 ([((prfx (Binding.name "simps"), []), [(simps, [])]), |
545 ([((prfx (Binding.name "simps"), []), [(simps, [])]), |