equal
deleted
inserted
replaced
134 |
134 |
135 val setup = |
135 val setup = |
136 Context.theory_map (Function_Common.set_preproc sequential_preproc) |
136 Context.theory_map (Function_Common.set_preproc sequential_preproc) |
137 |
137 |
138 |
138 |
139 val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), |
139 val fun_config = FunctionConfig { sequential=true, default=NONE, |
140 domintros=false, partials=false, tailrec=false } |
140 domintros=false, partials=false, tailrec=false } |
141 |
141 |
142 fun gen_add_fun add fixes statements config lthy = |
142 fun gen_add_fun add fixes statements config lthy = |
143 let |
143 let |
144 fun pat_completeness_auto ctxt = |
144 fun pat_completeness_auto ctxt = |