--- a/IntEx.thy	Thu Nov 26 21:16:59 2009 +0100
+++ b/IntEx.thy	Fri Nov 27 02:23:49 2009 +0100
@@ -174,7 +174,7 @@
 *)
 
 ML {*
-  mk_REGULARIZE_goal @{context} 
+  mk_regularize_trm @{context} 
     @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"}
     @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"}
   |> Syntax.string_of_term @{context}