106 val specs = (get_specs prednames) @ fun_pred_specs |
106 val specs = (get_specs prednames) @ fun_pred_specs |
107 val (intross3, thy''') = process_specification options specs thy' |
107 val (intross3, thy''') = process_specification options specs thy' |
108 val _ = print_intross options thy''' "Introduction rules with new constants: " intross3 |
108 val _ = print_intross options thy''' "Introduction rules with new constants: " intross3 |
109 val intross4 = map_specs (maps remove_pointless_clauses) intross3 |
109 val intross4 = map_specs (maps remove_pointless_clauses) intross3 |
110 val _ = print_intross options thy''' "After removing pointless clauses: " intross4 |
110 val _ = print_intross options thy''' "After removing pointless clauses: " intross4 |
111 val intross5 = |
111 val intross5 = map_specs (map (remove_equalities thy''')) intross4 |
112 map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4 |
112 val _ = print_intross options thy''' "After removing equality premises:" intross5 |
113 val intross6 = map_specs (map (expand_tuples thy''')) intross5 |
113 val intross6 = |
114 val intross7 = map_specs (map (eta_contract_ho_arguments thy''')) intross6 |
114 map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross5 |
115 val _ = print_intross options thy''' "introduction rules before registering: " intross7 |
115 val intross7 = map_specs (map (expand_tuples thy''')) intross6 |
|
116 val intross8 = map_specs (map (eta_contract_ho_arguments thy''')) intross7 |
|
117 val _ = print_intross options thy''' "introduction rules before registering: " intross8 |
116 val _ = print_step options "Registering introduction rules..." |
118 val _ = print_step options "Registering introduction rules..." |
117 val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' |
119 val thy'''' = fold Predicate_Compile_Core.register_intros intross8 thy''' |
118 in |
120 in |
119 thy'''' |
121 thy'''' |
120 end; |
122 end; |
121 |
123 |
122 fun preprocess options t thy = |
124 fun preprocess options t thy = |