equal
deleted
inserted
replaced
193 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) = |
193 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) = |
194 case AList.lookup (op =) fns i of |
194 case AList.lookup (op =) fns i of |
195 NONE => |
195 NONE => |
196 let |
196 let |
197 val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined", |
197 val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined", |
198 replicate ((length cargs) + (length (List.filter is_rec_type cargs))) |
198 replicate (length cargs + length (filter is_rec_type cargs)) |
199 dummyT ---> HOLogic.unitT)) constrs; |
199 dummyT ---> HOLogic.unitT)) constrs; |
200 val _ = warning ("No function definition for datatype " ^ quote tname) |
200 val _ = warning ("No function definition for datatype " ^ quote tname) |
201 in |
201 in |
202 (dummy_fns @ fs, defs) |
202 (dummy_fns @ fs, defs) |
203 end |
203 end |