diff -r d676974e3c89 -r 8bc7428745ad IntEx.thy --- 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 "\i j k. my_plus (my_plus i j) k \ my_plus i (my_plus j k)"} @{term "\i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |> Syntax.string_of_term @{context}