# HG changeset patch
# User wenzelm
# Date 1159479750 -7200
# Node ID 9913d3bc3d1720c139f2476bc08ce03179244728
# Parent  807c5f7dcb94eb32b0288b25ff0641b524ececa2
tuned;

diff -r 807c5f7dcb94 -r 9913d3bc3d17 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Sep 28 21:01:13 2006 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 28 23:42:30 2006 +0200
@@ -7,9 +7,7 @@
 
 theory HOL
 imports CPure
-uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
-    "Tools/res_atpset.ML"
-
+uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") "Tools/res_atpset.ML"
 begin
 
 subsection {* Primitive logic *}
@@ -920,7 +918,7 @@
 setup hypsubst_setup
 setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *}
 setup Classical.setup
-setup ResAtpSet.setup
+setup ResAtpset.setup
 setup clasetup
 
 lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"