diff -r 7a1518c42c56 -r 5048b02c2bbb src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Nov 18 15:01:00 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Nov 18 15:51:35 2009 -0800
@@ -320,14 +320,16 @@
       Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ typ_consts);
     val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2);
     fun free a = Free (Library.unprefix "'" a, deflT);
-    fun mk_defl_spec (lhs, rhs) =
-      mk_eqs (defl_of_typ defl_tab' free lhs, defl_of_typ defl_tab' free rhs);
+    fun mk_defl_spec (lhsT, rhsT) =
+      mk_eqs (defl_of_typ defl_tab' free lhsT,
+              defl_of_typ defl_tab' free rhsT);
     val defl_specs = map mk_defl_spec dom_eqns;
 
     (* register recursive definition of type combinators *)
     val typ_binds = map (Binding.suffix_name "_typ" o #2) doms;
     val (typ_unfold_thms, thy3) = add_fixdefs (typ_binds ~~ defl_specs) thy2;
 
+    (* define types using deflation combinators *)
     fun make_repdef ((vs, tbind, mx, _), typ_const) thy =
       let
         fun tfree a = TFree (a, the (AList.lookup (op =) sorts a))
@@ -341,6 +343,23 @@
     val (REP_thms, thy4) =
       fold_map make_repdef (doms ~~ typ_consts) thy3;
 
+    (* FIXME: use theory data for this *)
+    val REP_simps = REP_thms @
+      @{thms REP_cfun REP_ssum REP_sprod REP_cprod REP_up
+             REP_upper REP_lower REP_convex};
+
+    (* prove REP equations *)
+    fun mk_REP_eqn_thm (lhsT, rhsT) =
+      let
+        val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT);
+        val tac =
+          simp_tac (HOL_basic_ss addsimps REP_simps) 1
+          THEN resolve_tac typ_unfold_thms 1;
+      in
+        Goal.prove_global thy4 [] [] goal (K tac)
+      end;
+    val REP_eqn_thms = map mk_REP_eqn_thm dom_eqns;
+
   in
     thy4
   end;