--- a/Quot/Examples/SigmaEx.thy	Tue Jan 26 14:08:47 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Tue Jan 26 14:48:25 2010 +0100
@@ -130,7 +130,7 @@
   
 
 lemma liftd: "
-\<exists>\<exists>(hom_o, (hom_d, (hom_e, hom_m))).
+\<exists>\<exists>(hom_o, hom_d, hom_e, hom_m).
 (
  (\<forall>x. hom_o (Var x) = fvar x) \<and>
  (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and>
@@ -142,9 +142,7 @@
  (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
 )"
 apply (lifting tolift)
-apply (regularize)
-apply (simp)
-sorry
+done
 
 lemma tolift':
 "\<forall> fvar.