diff -r 64f9c76f70c7 -r 35436401f00d Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Sat Dec 26 23:20:46 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sun Dec 27 23:33:10 2009 +0100
@@ -234,16 +234,17 @@
 (* type variables ?'a1.0 (which are turned into frees *)
 (* 'a_1                                               *)
 lemma concat1: 
-  shows "concat [] = []"
+  shows "concat [] \<approx> []"
 by (simp)
 
 lemma concat2: 
-  shows "concat (x # xs) =  x @ concat xs"
+  shows "concat (x # xs) \<approx>  x @ concat xs"
 by (simp)
 
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
-apply(lifting concat1)
+apply(lifting_setup concat1)
+apply(regularize)
 apply(injection)
 defer
 apply(cleaning)