# HG changeset patch
# User haftmann
# Date 1133886386 -3600
# Node ID e8b7e0a2272780ffeee64382e9f4c50be1a00b49
# Parent  3126d01e9e359d1f2f166314eab54ddd297139a1
removed thms 'swap' and 'nth_map' from ML toplevel

diff -r 3126d01e9e35 -r e8b7e0a22727 src/HOL/List.ML
--- 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";
diff -r 3126d01e9e35 -r e8b7e0a22727 src/HOL/Tools/primrec_package.ML
--- 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);
diff -r 3126d01e9e35 -r e8b7e0a22727 src/HOL/cladata.ML
--- 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]
diff -r 3126d01e9e35 -r e8b7e0a22727 src/HOLCF/FOCUS/Fstream.ML
--- 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 ())