equal
deleted
inserted
replaced
172 let |
172 let |
173 val ty = fastype_of x |
173 val ty = fastype_of x |
174 in |
174 in |
175 if arg_no mem args_in_bn then |
175 if arg_no mem args_in_bn then |
176 (if is_rec_type dt then |
176 (if is_rec_type dt then |
177 (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: not good") |
177 (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.") |
178 else @{term "{} :: atom set"}) else |
178 else @{term "{} :: atom set"}) else |
179 if is_atom thy ty then mk_single_atom x else |
179 if is_atom thy ty then mk_single_atom x else |
180 if is_atom_set thy ty then mk_atoms x else |
180 if is_atom_set thy ty then mk_atoms x else |
181 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
181 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
182 @{term "{} :: atom set"} |
182 @{term "{} :: atom set"} |