--- a/src/HOL/List.ML Tue Dec 06 17:11:40 2005 +0100
+++ b/src/HOL/List.ML Tue Dec 06 17:26:26 2005 +0100
@@ -139,7 +139,6 @@
val nth_list_update = thm "nth_list_update";
val nth_list_update_eq = thm "nth_list_update_eq";
val nth_list_update_neq = thm "nth_list_update_neq";
-val nth_map = thm "nth_map";
val nth_map_upt = thm "nth_map_upt";
val nth_mem = thm "nth_mem";
val nth_replicate = thm "nth_replicate";
--- a/src/HOL/Tools/primrec_package.ML Tue Dec 06 17:11:40 2005 +0100
+++ b/src/HOL/Tools/primrec_package.ML Tue Dec 06 17:26:26 2005 +0100
@@ -230,15 +230,14 @@
val tnames = distinct (map (#1 o snd) rec_eqns);
val dts = find_dts dt_info tnames tnames;
val main_fns =
- map (fn (tname, {index, ...}) =>
- (index,
- fst (valOf (find_first (fn f => #1 (snd f) = tname) rec_eqns))))
- dts;
+ map (fn (tname, {index, ...}) =>
+ (index,
+ (fst o the o find_first (fn f => (#1 o snd) f = tname)) rec_eqns))
+ dts;
val {descr, rec_names, rec_rewrites, ...} =
- if null dts then
- primrec_err ("datatypes " ^ commas_quote tnames ^
- "\nare not mutually recursive")
- else snd (hd dts);
+ if null dts then
+ primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
+ else snd (hd dts);
val (fnameTs, fnss) = foldr (process_fun sg descr rec_eqns)
([], []) main_fns;
val (fs, defs) = foldr (get_fns fnss) ([], []) (descr ~~ rec_names);
--- a/src/HOL/cladata.ML Tue Dec 06 17:11:40 2005 +0100
+++ b/src/HOL/cladata.ML Tue Dec 06 17:26:26 2005 +0100
@@ -58,9 +58,11 @@
structure Classical = ClassicalFun(Classical_Data);
structure BasicClassical: BASIC_CLASSICAL = Classical;
-open BasicClassical;
-bind_thm ("contrapos_np", inst "Pa" "?Q" swap);
+open BasicClassical;
+val swap = Library.swap; (*unshadow basic library*)
+
+val _ = bind_thm ("contrapos_np", inst "Pa" "?Q" BasicClassical.swap);
(*Propositional rules*)
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
--- a/src/HOLCF/FOCUS/Fstream.ML Tue Dec 06 17:11:40 2005 +0100
+++ b/src/HOLCF/FOCUS/Fstream.ML Tue Dec 06 17:26:26 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 swap),
+ ALLGOALS(etac BasicClassical.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 swap 1,
+ etac BasicClassical.swap 1,
fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
qed_goal "slen_fscons_less_eq" (the_context ())