removed thms 'swap' and 'nth_map' from ML toplevel
authorhaftmann
Tue Dec 06 17:26:26 2005 +0100 (2005-12-06)
changeset 18362e8b7e0a22727
parent 18361 3126d01e9e35
child 18363 0040ee0b01c9
removed thms 'swap' and 'nth_map' from ML toplevel
src/HOL/List.ML
src/HOL/Tools/primrec_package.ML
src/HOL/cladata.ML
src/HOLCF/FOCUS/Fstream.ML
     1.1 --- a/src/HOL/List.ML	Tue Dec 06 17:11:40 2005 +0100
     1.2 +++ b/src/HOL/List.ML	Tue Dec 06 17:26:26 2005 +0100
     1.3 @@ -139,7 +139,6 @@
     1.4  val nth_list_update = thm "nth_list_update";
     1.5  val nth_list_update_eq = thm "nth_list_update_eq";
     1.6  val nth_list_update_neq = thm "nth_list_update_neq";
     1.7 -val nth_map = thm "nth_map";
     1.8  val nth_map_upt = thm "nth_map_upt";
     1.9  val nth_mem = thm "nth_mem";
    1.10  val nth_replicate = thm "nth_replicate";
     2.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Dec 06 17:11:40 2005 +0100
     2.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Dec 06 17:26:26 2005 +0100
     2.3 @@ -230,15 +230,14 @@
     2.4      val tnames = distinct (map (#1 o snd) rec_eqns);
     2.5      val dts = find_dts dt_info tnames tnames;
     2.6      val main_fns = 
     2.7 -	map (fn (tname, {index, ...}) =>
     2.8 -	     (index, 
     2.9 -	      fst (valOf (find_first (fn f => #1 (snd f) = tname) rec_eqns))))
    2.10 -	dts;
    2.11 +      map (fn (tname, {index, ...}) =>
    2.12 +        (index, 
    2.13 +          (fst o the o find_first (fn f => (#1 o snd) f = tname)) rec_eqns))
    2.14 +      dts;
    2.15      val {descr, rec_names, rec_rewrites, ...} = 
    2.16 -	if null dts then
    2.17 -	    primrec_err ("datatypes " ^ commas_quote tnames ^ 
    2.18 -			 "\nare not mutually recursive")
    2.19 -	else snd (hd dts);
    2.20 +      if null dts then
    2.21 +        primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
    2.22 +      else snd (hd dts);
    2.23      val (fnameTs, fnss) = foldr (process_fun sg descr rec_eqns)
    2.24  	                       ([], []) main_fns;
    2.25      val (fs, defs) = foldr (get_fns fnss) ([], []) (descr ~~ rec_names);
     3.1 --- a/src/HOL/cladata.ML	Tue Dec 06 17:11:40 2005 +0100
     3.2 +++ b/src/HOL/cladata.ML	Tue Dec 06 17:26:26 2005 +0100
     3.3 @@ -58,9 +58,11 @@
     3.4  structure Classical = ClassicalFun(Classical_Data);
     3.5  
     3.6  structure BasicClassical: BASIC_CLASSICAL = Classical; 
     3.7 -open BasicClassical;
     3.8  
     3.9 -bind_thm ("contrapos_np", inst "Pa" "?Q" swap);
    3.10 +open BasicClassical;
    3.11 +val swap = Library.swap; (*unshadow basic library*)
    3.12 +
    3.13 +val _ = bind_thm ("contrapos_np", inst "Pa" "?Q" BasicClassical.swap);
    3.14  
    3.15  (*Propositional rules*)
    3.16  val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
     4.1 --- a/src/HOLCF/FOCUS/Fstream.ML	Tue Dec 06 17:11:40 2005 +0100
     4.2 +++ b/src/HOLCF/FOCUS/Fstream.ML	Tue Dec 06 17:26:26 2005 +0100
     4.3 @@ -66,7 +66,7 @@
     4.4          "x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))" (fn _ => [
     4.5          simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS thm "stream_prefix'"])1,
     4.6          Step_tac 1,
     4.7 -         ALLGOALS(etac swap),
     4.8 +         ALLGOALS(etac BasicClassical.swap),
     4.9           fast_tac (HOL_cs addIs [refl_less] addEs [DefE]) 2,
    4.10          rtac Lift_cases 1,
    4.11           contr_tac 1,
    4.12 @@ -139,7 +139,7 @@
    4.13          step_tac (HOL_cs addSEs [DefE]) 1,
    4.14          step_tac (HOL_cs addSEs [DefE]) 1,
    4.15          step_tac (HOL_cs addSEs [DefE]) 1,
    4.16 -        etac swap 1,
    4.17 +        etac BasicClassical.swap 1,
    4.18          fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
    4.19  
    4.20  qed_goal "slen_fscons_less_eq" (the_context ())