--- 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]
--- 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 ())