# HG changeset patch
# User paulson
# Date 864644025 -7200
# Node ID 4e7dfe8ae41baa4fbcc7c9c2cef828a9743adeaf
# Parent  5101517c26141bae051e3dafc16384c0c6f286eb
Added a missing "result();" after problem 43.

diff -r 5101517c2614 -r 4e7dfe8ae41b src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Mon May 26 12:44:04 1997 +0200
+++ b/src/HOL/ex/cla.ML	Mon May 26 12:53:45 1997 +0200
@@ -347,7 +347,7 @@
     "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \
 \ --> (! x. (! y. q x y = (q y x::bool)))";
 by (Blast_tac 1);
-
+result();
 
 writeln"Problem 44";
 goal HOL.thy "(! x. f(x) -->                                    \