removed unnecessary theory qualifiers;

--- a/src/ZF/Induct/Primrec.thy	Mon Feb 11 21:32:11 2008 +0100
+++ b/src/ZF/Induct/Primrec.thy	Mon Feb 11 21:32:12 2008 +0100
@@ -31,7 +31,7 @@
 
 definition
   COMP :: "[i,i]=>i"  where
-  "COMP(g,fs) == \<lambda>l \<in> list(nat). g ` List_ZF.map(\<lambda>f. f`l, fs)"
+  "COMP(g,fs) == \<lambda>l \<in> list(nat). g ` map(\<lambda>f. f`l, fs)"
 
 definition
   PREC :: "[i,i]=>i"  where
@@ -93,7 +93,7 @@
   monos list_mono
   con_defs SC_def CONSTANT_def PROJ_def COMP_def PREC_def
   type_intros nat_typechecks list.intros
-    lam_type list_case_type drop_type List_ZF.map_type
+    lam_type list_case_type drop_type map_type
     apply_type rec_type
 
 

--- a/src/ZF/Induct/Term.thy	Mon Feb 11 21:32:11 2008 +0100
+++ b/src/ZF/Induct/Term.thy	Mon Feb 11 21:32:12 2008 +0100
@@ -235,7 +235,7 @@
   \medskip Theorems about @{text term_map}.
 *}
 
-declare List_ZF.map_compose [simp]
+declare map_compose [simp]
 
 lemma term_map_ident: "t \<in> term(A) ==> term_map(\<lambda>u. u, t) = t"
   by (induct rule: term_induct_eqn) simp

--- a/src/ZF/UNITY/Monotonicity.thy	Mon Feb 11 21:32:11 2008 +0100
+++ b/src/ZF/UNITY/Monotonicity.thy	Mon Feb 11 21:32:12 2008 +0100
@@ -69,7 +69,7 @@
 lemma take_mono_left:
      "[| i le j; xs \<in> list(A); j \<in> nat |]
       ==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
-by (blast intro: Nat_ZF.le_in_nat take_mono_left_lemma) 
+by (blast intro: le_in_nat take_mono_left_lemma) 
 
 lemma take_mono_right:
      "[| <xs,ys> \<in> prefix(A); i \<in> nat |] 

--- a/src/ZF/ind_syntax.ML	Mon Feb 11 21:32:11 2008 +0100
+++ b/src/ZF/ind_syntax.ML	Mon Feb 11 21:32:12 2008 +0100
@@ -127,7 +127,7 @@
           (fn t => "Datatype set not previously declared as constant: " ^
                    Sign.string_of_term @{theory IFOL} t);
         val rec_names = (*nat doesn't have to be added*)
-	    @{const_name "Nat_ZF.nat"} :: map (#1 o dest_Const) rec_hds
+	    @{const_name "nat"} :: map (#1 o dest_Const) rec_hds
 	val u = if co then quniv else univ
 	val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
           (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t

--- a/src/ZF/int_arith.ML	Mon Feb 11 21:32:11 2008 +0100
+++ b/src/ZF/int_arith.ML	Mon Feb 11 21:32:12 2008 +0100
@@ -111,11 +111,11 @@
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
 val zero = mk_numeral 0;
-val mk_plus = FOLogic.mk_binop @{const_name "Int_ZF.zadd"};
+val mk_plus = FOLogic.mk_binop @{const_name "zadd"};
 
 val iT = Ind_Syntax.iT;
 
-val zminus_const = Const (@{const_name "Int_ZF.zminus"}, iT --> iT);
+val zminus_const = Const (@{const_name "zminus"}, iT --> iT);
 
 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
@@ -126,30 +126,30 @@
 fun long_mk_sum []        = zero
   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
-val dest_plus = FOLogic.dest_bin @{const_name "Int_ZF.zadd"} iT;
+val dest_plus = FOLogic.dest_bin @{const_name "zadd"} iT;
 
 (*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const (@{const_name "Int_ZF.zadd"}, _) $ t $ u, ts) =
+fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (pos, u, ts))
-  | dest_summing (pos, Const (@{const_name "Int_ZF.zdiff"}, _) $ t $ u, ts) =
+  | dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (not pos, u, ts))
   | dest_summing (pos, t, ts) =
         if pos then t::ts else zminus_const$t :: ts;
 
 fun dest_sum t = dest_summing (true, t, []);
 
-val mk_diff = FOLogic.mk_binop @{const_name "Int_ZF.zdiff"};
-val dest_diff = FOLogic.dest_bin @{const_name "Int_ZF.zdiff"} iT;
+val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
+val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} iT;
 
 val one = mk_numeral 1;
-val mk_times = FOLogic.mk_binop @{const_name "Int_ZF.zmult"};
+val mk_times = FOLogic.mk_binop @{const_name "zmult"};
 
 fun mk_prod [] = one
   | mk_prod [t] = t
   | mk_prod (t :: ts) = if t = one then mk_prod ts
                         else mk_times (t, mk_prod ts);
 
-val dest_times = FOLogic.dest_bin @{const_name "Int_ZF.zmult"} iT;
+val dest_times = FOLogic.dest_bin @{const_name "zmult"} iT;
 
 fun dest_prod t =
       let val (t,u) = dest_times t
@@ -160,7 +160,7 @@
 fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
 
 (*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff sign (Const (@{const_name "Int_ZF.zminus"}, _) $ t) = dest_coeff (~sign) t
+fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t
   | dest_coeff sign t =
     let val ts = sort Term.term_ord (dest_prod t)
         val (n, ts') = find_first_numeral [] ts
@@ -254,8 +254,8 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binrel @{const_name "Int_ZF.zless"}
-  val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zless"} iT
+  val mk_bal   = FOLogic.mk_binrel @{const_name "zless"}
+  val dest_bal = FOLogic.dest_bin @{const_name "zless"} iT
   val bal_add1 = less_add_iff1 RS iff_trans
   val bal_add2 = less_add_iff2 RS iff_trans
 );
@@ -263,8 +263,8 @@
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binrel @{const_name "Int_ZF.zle"}
-  val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zle"} iT
+  val mk_bal   = FOLogic.mk_binrel @{const_name "zle"}
+  val dest_bal = FOLogic.dest_bin @{const_name "zle"} iT
   val bal_add1 = le_add_iff1 RS iff_trans
   val bal_add2 = le_add_iff2 RS iff_trans
 );