equal
deleted
inserted
replaced
168 val options = extract_options (((expected_modes, proposed_modes), raw_options), const) |
168 val options = extract_options (((expected_modes, proposed_modes), raw_options), const) |
169 in |
169 in |
170 if (is_inductify options) then |
170 if (is_inductify options) then |
171 let |
171 let |
172 val lthy' = Local_Theory.theory (preprocess options t) lthy |
172 val lthy' = Local_Theory.theory (preprocess options t) lthy |
173 |> Local_Theory.checkpoint |
|
174 val const = |
173 val const = |
175 case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of |
174 case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of |
176 SOME c => c |
175 SOME c => c |
177 | NONE => const |
176 | NONE => const |
178 val _ = print_step options "Starting Predicate Compile Core..." |
177 val _ = print_step options "Starting Predicate Compile Core..." |