392 (* definitions of raw permutations *) |
392 (* definitions of raw permutations *) |
393 val ((perms, raw_perm_defs, raw_perm_simps), lthy2) = |
393 val ((perms, raw_perm_defs, raw_perm_simps), lthy2) = |
394 if get_STEPS lthy1 > 2 |
394 if get_STEPS lthy1 > 2 |
395 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
395 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
396 else raise TEST lthy1 |
396 else raise TEST lthy1 |
397 |
397 |
398 val (_, lthy2a) = Local_Theory.note ((Binding.empty, |
398 (* noting the raw permutations as eqvt theorems *) |
399 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_defs) lthy2; |
399 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
|
400 val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_defs) lthy2 |
400 |
401 |
401 val thy = Local_Theory.exit_global lthy2a; |
402 val thy = Local_Theory.exit_global lthy2a; |
402 val thy_name = Context.theory_name thy |
403 val thy_name = Context.theory_name thy |
403 |
404 |
404 (* definition of raw fv_functions *) |
405 (* definition of raw fv_functions *) |