218 fun distill lthy fixes eqs = |
218 fun distill lthy fixes eqs = |
219 let |
219 let |
220 val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v |
220 val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v |
221 orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs []; |
221 orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs []; |
222 val tnames = distinct (op =) (map (#1 o snd) eqns); |
222 val tnames = distinct (op =) (map (#1 o snd) eqns); |
223 val dts = find_dts (Datatype.get_datatypes (ProofContext.theory_of lthy)) tnames tnames; |
223 val dts = find_dts (Datatype.get_all (ProofContext.theory_of lthy)) tnames tnames; |
224 val main_fns = map (fn (tname, {index, ...}) => |
224 val main_fns = map (fn (tname, {index, ...}) => |
225 (index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts; |
225 (index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts; |
226 val {descr, rec_names, rec_rewrites, ...} = |
226 val {descr, rec_names, rec_rewrites, ...} = |
227 if null dts then primrec_error |
227 if null dts then primrec_error |
228 ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive") |
228 ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive") |