src/HOLCF/domain/theorems.ML

                                 mk_trp(defined(con_app con args)))) ([
                           rtac rev_contrapos 1, 
                           eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
                           asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons;
 val con_rews = con_stricts @ con_defins;
+
+val con_compacts =
+  let
+    val rules = [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
+    fun one_compact (con,args) = pg con_appls
+      (lift (fn x => %%:compactN $ %:(vname x)) (args, mk_trp(%%:compactN $ (con_app con args))))
+      [rtac (iso_locale RS iso_compact_abs) 1, REPEAT (resolve_tac rules 1 ORELSE atac 1)];
+  in map one_compact cons end;
 
 val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%:sel))) [
                                 simp_tac (HOLCF_ss addsimps when_rews) 1];
 in List.concat(map (fn (_,args) => List.mapPartial (fn arg => Option.map one_sel (sel_of arg)) args) cons) end;
 val sel_apps = let fun one_sel c n sel = map (fn (con,args) => 

        |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
 		("iso_rews" , iso_rews  ),
 		("exhaust"  , [exhaust] ),
 		("casedist" , [casedist]),
 		("when_rews", when_rews ),
+		("compacts", con_compacts),
 		("con_rews", con_rews),
 		("sel_rews", sel_rews),
 		("dis_rews", dis_rews),
 		("dist_les", dist_les),
 		("dist_eqs", dist_eqs),