27 (* permutations for quotient types *)

    28 

    29 ML {*

    30 fun quotient_lift_consts_export qtys spec ctxt =

    31 let

    32   val (result, ctxt') = fold_map (Quotient_Def.lift_raw_const qtys) spec ctxt;

    33   val (ts_loc, defs_loc) = split_list (map (fn info => (#qconst info, #def info)) result);

    34   val morphism = ProofContext.export_morphism ctxt' ctxt;

    35   val ts = map (Morphism.term morphism) ts_loc

    36   val defs = Morphism.fact morphism defs_loc

    37 in

    38   (ts, defs, ctxt')

    40 *}

    41 

    42 

    43 

    44 ML {*

    45 fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =

    46 let

    47   val lthy =

    48     Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;

    49   val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy;

    50   val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;

    51   fun tac _ =

    52     Class.intro_classes_tac [] THEN

    53     (ALLGOALS (resolve_tac lifted_thms))

    54   val lthy'' = Class.prove_instantiation_instance tac lthy'

    55 in

    56   Local_Theory.exit_global lthy''

    57 end

    58 *}

    59 

    60 

    61 end