# HG changeset patch
# User wenzelm
# Date 1134042603 -3600
# Node ID 2f9b2539c5bbf87ef6bb52b90dae81ad2b52a9db
# Parent  c209f4b61b5101328056c0ce7c3c7733bf70786a
Classical.swap;

diff -r c209f4b61b51 -r 2f9b2539c5bb src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Thu Dec 08 12:50:02 2005 +0100
+++ b/src/HOL/cladata.ML	Thu Dec 08 12:50:03 2005 +0100
@@ -60,9 +60,9 @@
 structure BasicClassical: BASIC_CLASSICAL = Classical; 
 
 open BasicClassical;
-val swap = Library.swap; (*unshadow basic library*)
+val swap = Library.swap;
 
-val _ = bind_thm ("contrapos_np", inst "Pa" "?Q" BasicClassical.swap);
+val _ = bind_thm ("contrapos_np", inst "Pa" "?Q" Classical.swap);
 
 (*Propositional rules*)
 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
diff -r c209f4b61b51 -r 2f9b2539c5bb src/HOLCF/FOCUS/Fstream.ML
--- a/src/HOLCF/FOCUS/Fstream.ML	Thu Dec 08 12:50:02 2005 +0100
+++ b/src/HOLCF/FOCUS/Fstream.ML	Thu Dec 08 12:50:03 2005 +0100
@@ -66,7 +66,7 @@
         "x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))" (fn _ => [
         simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS thm "stream_prefix'"])1,
         Step_tac 1,
-         ALLGOALS(etac BasicClassical.swap),
+         ALLGOALS(etac Classical.swap),
          fast_tac (HOL_cs addIs [refl_less] addEs [DefE]) 2,
         rtac Lift_cases 1,
          contr_tac 1,
@@ -139,7 +139,7 @@
         step_tac (HOL_cs addSEs [DefE]) 1,
         step_tac (HOL_cs addSEs [DefE]) 1,
         step_tac (HOL_cs addSEs [DefE]) 1,
-        etac BasicClassical.swap 1,
+        etac Classical.swap 1,
         fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
 
 qed_goal "slen_fscons_less_eq" (the_context ())