equal
deleted
inserted
replaced
160 [] => () |
160 [] => () |
161 | xs => error ("Missing equivariance theorem for predicate(s): " ^ |
161 | xs => error ("Missing equivariance theorem for predicate(s): " ^ |
162 commas_quote xs)); |
162 commas_quote xs)); |
163 val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the |
163 val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the |
164 (Induct.lookup_inductP ctxt (hd names))))); |
164 (Induct.lookup_inductP ctxt (hd names))))); |
165 val ([raw_induct'], ctxt') = Variable.import_terms false [Thm.prop_of raw_induct] ctxt; |
165 val (raw_induct', ctxt') = ctxt |
|
166 |> yield_singleton (Variable.import_terms false) (Thm.prop_of raw_induct); |
166 val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> |
167 val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> |
167 HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb); |
168 HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb); |
168 val ps = map (fst o snd) concls; |
169 val ps = map (fst o snd) concls; |
169 |
170 |
170 val _ = (case duplicates (op = o apply2 fst) avoids of |
171 val _ = (case duplicates (op = o apply2 fst) avoids of |