equal
deleted
inserted
replaced
151 fun gen_fun add config fixes statements int lthy = |
151 fun gen_fun add config fixes statements int lthy = |
152 lthy |
152 lthy |
153 |> add fixes statements config |
153 |> add fixes statements config |
154 |> by_pat_completeness_auto int |
154 |> by_pat_completeness_auto int |
155 |> Local_Theory.restore |
155 |> Local_Theory.restore |
156 |> termination_by (Function_Common.get_termination_prover lthy) int |
156 |> termination_by (SIMPLE_METHOD o Function_Common.get_termination_prover lthy) int |
157 |
157 |
158 val add_fun = gen_fun Function.function |
158 val add_fun = gen_fun Function.function |
159 val add_fun_cmd = gen_fun Function.function_cmd |
159 val add_fun_cmd = gen_fun Function.function_cmd |
160 |
160 |
161 |
161 |