372 const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11 |
372 const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11 |
373 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts |
373 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts |
374 val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12; |
374 val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12; |
375 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
375 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
376 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
376 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
377 val thy = Local_Theory.exit_global lthy12b; |
377 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
|
378 val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
|
379 val thy = Local_Theory.exit_global lthy12c; |
378 val perm_names = map (fn x => "permute_" ^ x) qty_names |
380 val perm_names = map (fn x => "permute_" ^ x) qty_names |
379 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
381 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
380 val lthy13 = Theory_Target.init NONE thy'; |
382 val lthy13 = Theory_Target.init NONE thy'; |
381 in |
383 in |
382 if !restricted_nominal = 0 then |
384 if !restricted_nominal = 0 then |