equal
deleted
inserted
replaced
144 val raw_induct = atomize_induct ctxt raw_induct |
144 val raw_induct = atomize_induct ctxt raw_induct |
145 val intros = map atomize_intr intrs |
145 val intros = map atomize_intr intrs |
146 val params_no = length (Inductive.params_of raw_induct) |
146 val params_no = length (Inductive.params_of raw_induct) |
147 val (([raw_concl], [raw_pi]), ctxt') = ctxt |
147 val (([raw_concl], [raw_pi]), ctxt') = ctxt |
148 |> Variable.import_terms false [concl_of raw_induct] |
148 |> Variable.import_terms false [concl_of raw_induct] |
149 ||>> Variable.variant_fixes ["pi"] |
149 ||>> Variable.variant_fixes ["p"] |
150 val pi = Free (raw_pi, @{typ perm}) |
150 val pi = Free (raw_pi, @{typ perm}) |
151 val preds = map (fst o HOLogic.dest_imp) |
151 val preds = map (fst o HOLogic.dest_imp) |
152 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
152 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
153 val goal = HOLogic.mk_Trueprop |
153 val goal = HOLogic.mk_Trueprop |
154 (foldr1 HOLogic.mk_conj (map (prepare_goal params_no pi) preds)) |
154 (foldr1 HOLogic.mk_conj (map (prepare_goal params_no pi) preds)) |