681 ML {*

   682   fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)

   683   val consts = [@{const_name "Nil"}]

   684 *}

   685 

   686 ML {*

   687 fun build_goal thm constructors mk_rep_abs =

   688   let

   689     fun is_const (Const (x, t)) = x mem constructors

   690       | is_const _ = false

   691     fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))

   692       | build_aux (f $ a) =

   693           (if is_const f then mk_rep_abs (f $ (build_aux a))

   694           else ((build_aux f) $ (build_aux a)))

   695       | build_aux x =

   696           if is_const x then mk_rep_abs x else x

   697     val concl = Thm.concl_of thm

   698   in

   699   HOLogic.mk_eq ((build_aux concl), concl)

   700 end *}

   701 

   702 ML {*

   703 val no_vars = Thm.rule_attribute (fn context => fn th =>

   704   let

   705     val ctxt = Variable.set_body false (Context.proof_of context);

   706     val ((_, [th']), _) = Variable.import true [th] ctxt;

   707   in th' end);

   708 *}

   709 

   710 ML {*

   711   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))

   712   val goal = build_goal m1_novars consts mk_rep_abs

   713   val cgoal = cterm_of @{theory} goal

   714 *}

   715 

   716 ML {* val emptyt = symmetric @{thm EMPTY_def} *}

   717 ML {* MetaSimplifier.rewrite false [emptyt] cgoal *}