# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1258968419 -3600
# Node ID 7851e2a74f850c8a005b3375fbb44d2bfd4c3572
# Parent  87f5fbebd6d53c81104d16792372ccef1840edc8
The other branch does not seem to work...

diff -r 87f5fbebd6d5 -r 7851e2a74f85 FSet.thy
--- 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