--- a/FSet.thy	Mon Nov 23 13:24:12 2009 +0100
+++ b/FSet.thy	Mon Nov 23 13:46:14 2009 +0100
@@ -603,10 +603,9 @@
   |> writeln
 *}
 
-ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} 
+ML {* val tta = 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 *}