149   fun tac _ (_, _, simps) =

   149   fun tac _ (_, _, simps) =

   150     Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)

   150     Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)

   151   

   151   

   152   fun morphism phi (fvs, dfs, simps) =

   152   fun morphism phi (fvs, dfs, simps) =

   153     (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps);

   153     (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps);

   156 in

   154 in

   157   lthy'

   155   lthy'

   159   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))

   156   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))

   160   |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))

   157   |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))

   161   |> Class_Target.prove_instantiation_exit_result morphism tac 

   158   |> Class_Target.prove_instantiation_exit_result morphism tac 

   162        (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms')

   159        (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms')

   163 end

   160 end

   166 

   163 

   167 

   164 

   168 

   165 

   169 

   166 

   170 (* permutations for quotient types *)

   167 (* permutations for quotient types *)

   171 

   170 

   172 ML {*

   171 ML {*

   173 fun quotient_lift_consts_export qtys spec ctxt =

   172 fun quotient_lift_consts_export qtys spec ctxt =

   174 let

   173 let

   175   val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;

   174   val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;