src/HOLCF/domain/theorems.ML

--- a/src/HOLCF/domain/theorems.ML	Wed May 03 02:16:23 2006 +0200
+++ b/src/HOLCF/domain/theorems.ML	Wed May 03 03:46:25 2006 +0200
@@ -310,27 +310,22 @@
     let
       fun append s = upd_vname(fn v => v^s);
       val (largs,rargs) = (args, map (append "'") args);
-      val concl = mk_trp (foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs)));
-      val prem = mk_trp (rel(con_app con largs,con_app con rargs));
-      val prop = prem ===> lift_defined %: (nonlazy largs, concl);
+      val concl = foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs));
+      val prem = rel (con_app con largs, con_app con rargs);
+      val sargs = case largs of [_] => [] | _ => nonlazy args;
+      val prop = lift_defined %: (sargs, mk_trp (prem === concl));
     in pg con_appls prop end;
   val cons' = List.filter (fn (_,args) => args<>[]) cons;
 in
 val inverts =
   let
-    val abs_less = ax_abs_iso RS (allI RS injection_less) RS iffD1;
-    val tacs = [
-      dtac abs_less 1,
-      REPEAT (dresolve_tac [sinl_less RS iffD1, sinr_less RS iffD1] 1),
-      asm_full_simp_tac (HOLCF_ss addsimps [spair_less]) 1];
+    val abs_less = ax_abs_iso RS (allI RS injection_less);
+    val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
   in map (fn (con,args) => pgterm (op <<) con args tacs) cons' end;
 val injects =
   let
-    val abs_eq = ax_abs_iso RS (allI RS injection_eq) RS iffD1;
-    val tacs = [
-      dtac abs_eq 1,
-      REPEAT (dresolve_tac [sinl_inject, sinr_inject] 1),
-      asm_full_simp_tac (HOLCF_ss addsimps [spair_eq]) 1];
+    val abs_eq = ax_abs_iso RS (allI RS injection_eq);
+    val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
   in map (fn (con,args) => pgterm (op ===) con args tacs) cons' end;
 end;