--- a/FSet.thy	Mon Nov 23 10:04:35 2009 +0100
+++ b/FSet.thy	Mon Nov 23 10:26:59 2009 +0100
@@ -587,6 +587,10 @@
 ML {* prop_of t_a *}
 ML {* term_of glac *}
 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 {* val tt = Syntax.check_term @{context} tta *}
 
 prove t_r: {* Logic.mk_implies