--- a/FSet.thy	Mon Nov 23 10:26:59 2009 +0100
+++ b/FSet.thy	Mon Nov 23 13:24:12 2009 +0100
@@ -377,6 +377,8 @@
 
 thm list.recs(2)
 ML {* val t_a = atomize_thm @{thm list_induct_part} *}
+
+
 (* prove {* build_regularize_goal t_a rty rel @{context}  *}
  ML_prf {*  fun tac ctxt = FIRST' [
       rtac rel_refl,
@@ -384,7 +386,7 @@
       rtac @{thm universal_twice},
       (rtac @{thm impI} THEN' atac),
       rtac @{thm implication_twice},
-      (*rtac @{thm equality_twice},*)
+      //comented out  rtac @{thm equality_twice}, //
       EqSubst.eqsubst_tac ctxt [0]
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])],
@@ -393,7 +395,7 @@
      ]; *}
   apply (atomize(full))
   apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
-  done*)
+  done  *)
 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
 ML {*
   val rt = build_repabs_term @{context} t_r consts rty qty
@@ -589,9 +591,24 @@
 ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *}
 
 (* Does not work. *)
-(* ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} *)
+ML {* 
+  prop_of t_a 
+  |> Syntax.string_of_term @{context}
+  |> writeln
+*}
+
+ML {* 
+  (term_of glac) 
+  |> Syntax.string_of_term @{context}
+  |> writeln
+*}
+
+ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} 
 
 ML {* val tt = Syntax.check_term @{context} tta *}
+ML {* val ttr = Syntax.check_term @{context} ttar *}
+
+
 
 prove t_r: {* Logic.mk_implies
        ((prop_of t_a), tt) *}