56 |
56 |
57 (* at class instance *) |
57 (* at class instance *) |
58 val lthy = |
58 val lthy = |
59 Class.instantiation ([full_tname], [], @{sort at}) thy; |
59 Class.instantiation ([full_tname], [], @{sort at}) thy; |
60 val ((_, (_, permute_ldef)), lthy) = |
60 val ((_, (_, permute_ldef)), lthy) = |
61 Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy; |
61 Specification.definition NONE [] [] ((permute_def_name, []), permute_eqn) lthy; |
62 val ((_, (_, atom_ldef)), lthy) = |
62 val ((_, (_, atom_ldef)), lthy) = |
63 Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; |
63 Specification.definition NONE [] [] ((atom_def_name, []), atom_eqn) lthy; |
64 val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); |
64 val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); |
65 val permute_def = singleton (Proof_Context.export lthy ctxt_thy) permute_ldef; |
65 val permute_def = singleton (Proof_Context.export lthy ctxt_thy) permute_ldef; |
66 val atom_def = singleton (Proof_Context.export lthy ctxt_thy) atom_ldef; |
66 val atom_def = singleton (Proof_Context.export lthy ctxt_thy) atom_ldef; |
67 val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; |
67 val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; |
68 val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def] |
68 val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def] |