51 val permute_def_name = |
51 val permute_def_name = |
52 Binding.prefix_name "permute_" (Binding.suffix_name "_def" name); |
52 Binding.prefix_name "permute_" (Binding.suffix_name "_def" name); |
53 |
53 |
54 (* at class instance *) |
54 (* at class instance *) |
55 val lthy = |
55 val lthy = |
56 Theory_Target.instantiation ([full_tname], [], @{sort at}) thy; |
56 Class.instantiation ([full_tname], [], @{sort at}) thy; |
57 val ((_, (_, permute_ldef)), lthy) = |
57 val ((_, (_, permute_ldef)), lthy) = |
58 Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy; |
58 Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy; |
59 val ((_, (_, atom_ldef)), lthy) = |
59 val ((_, (_, atom_ldef)), lthy) = |
60 Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; |
60 Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; |
61 val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); |
61 val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); |