# HG changeset patch
# User paulson
# Date 840446356 -7200
# Node ID 947a34e00d1ea21367abc9d144e759ec51018a26
# Parent  c27e624b6d872919ee6ddc9ebd88b0a7a83338d9
Now starts with set_current_thy

diff -r c27e624b6d87 -r 947a34e00d1e src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Mon Aug 19 11:18:36 1996 +0200
+++ b/src/HOL/ex/cla.ML	Mon Aug 19 11:19:16 1996 +0200
@@ -10,6 +10,8 @@
 
 writeln"File HOL/ex/cla.";
 
+set_current_thy "HOL";  (*Boosts efficiency by omitting redundant rules*)
+
 goal HOL.thy "(P --> Q | R) --> (P-->Q) | (P-->R)";
 by (Fast_tac 1);
 result();