--- a/QuotMain.thy	Tue Aug 25 10:35:28 2009 +0200
+++ b/QuotMain.thy	Tue Aug 25 14:37:11 2009 +0200
@@ -678,3 +678,40 @@
   apply (rule QUOT_TYPE_fset_i.thm10)
   done
 
+ML {*
+  fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
+  val consts = [@{const_name "Nil"}]
+*}
+
+ML {*
+fun build_goal thm constructors mk_rep_abs =
+  let
+    fun is_const (Const (x, t)) = x mem constructors
+      | is_const _ = false
+    fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
+      | build_aux (f $ a) =
+          (if is_const f then mk_rep_abs (f $ (build_aux a))
+          else ((build_aux f) $ (build_aux a)))
+      | build_aux x =
+          if is_const x then mk_rep_abs x else x
+    val concl = Thm.concl_of thm
+  in
+  HOLogic.mk_eq ((build_aux concl), concl)
+end *}
+
+ML {*
+val no_vars = Thm.rule_attribute (fn context => fn th =>
+  let
+    val ctxt = Variable.set_body false (Context.proof_of context);
+    val ((_, [th']), _) = Variable.import true [th] ctxt;
+  in th' end);
+*}
+
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
+  val goal = build_goal m1_novars consts mk_rep_abs
+  val cgoal = cterm_of @{theory} goal
+*}
+
+ML {* val emptyt = symmetric @{thm EMPTY_def} *}
+ML {* MetaSimplifier.rewrite false [emptyt] cgoal *}