equal
deleted
inserted
replaced
167 commas_quote xs)); |
167 commas_quote xs)); |
168 val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the |
168 val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the |
169 (Induct.lookup_inductP ctxt (hd names))))); |
169 (Induct.lookup_inductP ctxt (hd names))))); |
170 val induct_cases' = if null induct_cases then replicate (length intrs) "" |
170 val induct_cases' = if null induct_cases then replicate (length intrs) "" |
171 else induct_cases; |
171 else induct_cases; |
172 val ([raw_induct'], ctxt') = Variable.import_terms false [Thm.prop_of raw_induct] ctxt; |
172 val (raw_induct', ctxt') = ctxt |
|
173 |> yield_singleton (Variable.import_terms false) (Thm.prop_of raw_induct); |
173 val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> |
174 val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> |
174 HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb); |
175 HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb); |
175 val ps = map (fst o snd) concls; |
176 val ps = map (fst o snd) concls; |
176 |
177 |
177 val _ = (case duplicates (op = o apply2 fst) avoids of |
178 val _ = (case duplicates (op = o apply2 fst) avoids of |