tuned ML code (the_context, bind_thms(s));

--- a/src/ZF/Integ/Bin.ML	Thu Sep 07 21:18:18 2000 +0200
+++ b/src/ZF/Integ/Bin.ML	Thu Sep 07 21:21:07 2000 +0200
@@ -29,9 +29,10 @@
 by (asm_simp_tac (simpset() addsimps bin.case_eqns) 1);
 qed "NCons_BIT";
 
-val NCons_simps = [NCons_Pls_0, NCons_Pls_1, 
-		   NCons_Min_0, NCons_Min_1,
-		   NCons_BIT];
+bind_thms ("NCons_simps",
+ [NCons_Pls_0, NCons_Pls_1,
+  NCons_Min_0, NCons_Min_1,
+  NCons_BIT]);
 Addsimps NCons_simps;
 
 

--- a/src/ZF/Integ/EquivClass.ML	Thu Sep 07 21:18:18 2000 +0200
+++ b/src/ZF/Integ/EquivClass.ML	Thu Sep 07 21:21:07 2000 +0200
@@ -120,7 +120,7 @@
 **)
 
 (*Conversion rule*)
-val prems as [equivA,bcong,_] = goal EquivClass.thy
+val prems as [equivA,bcong,_] = goal (the_context ())
     "[| equiv(A,r);  congruent(r,b);  a: A |] ==> (UN x:r``{a}. b(x)) = b(a)";
 by (cut_facts_tac prems 1);
 by (rtac ([refl RS UN_cong, UN_constant] MRS trans) 1);
@@ -165,7 +165,7 @@
 by (Blast_tac 1);
 qed "congruent2_implies_congruent";
 
-val equivA::prems = goalw EquivClass.thy [congruent_def]
+val equivA::prems = goalw (the_context ()) [congruent_def]
     "[| equiv(A,r);  congruent2(r,b);  a: A |] ==> \
 \    congruent(r, %x1. UN x2:r``{a}. b(x1,x2))";
 by (cut_facts_tac (equivA::prems) 1);
@@ -178,7 +178,7 @@
 by (Blast_tac 1);
 qed "congruent2_implies_congruent_UN";
 
-val prems as equivA::_ = goal EquivClass.thy
+val prems as equivA::_ = goal (the_context ())
     "[| equiv(A,r);  congruent2(r,b);  a1: A;  a2: A |]  \
 \    ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
 by (cut_facts_tac prems 1);

--- a/src/ZF/Integ/Int.ML	Thu Sep 07 21:18:18 2000 +0200
+++ b/src/ZF/Integ/Int.ML	Thu Sep 07 21:21:07 2000 +0200
@@ -36,7 +36,7 @@
 by (Fast_tac 1);
 qed "intrelE_lemma";
 
-val [major,minor] = goal thy
+val [major,minor] = goal (the_context ())
   "[| p: intrel;  \
 \     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
 \                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
@@ -69,7 +69,7 @@
 	  add_0_right, add_succ_right];
 Addcongs [conj_cong];
 
-val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
+bind_thm ("eq_intrelD", equiv_intrel RSN (2,eq_equiv_class));
 
 (** int_of: the injection from nat to int **)
 
@@ -486,7 +486,7 @@
 qed "zadd_left_commute";
 
 (*Integer addition is an AC operator*)
-val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
+bind_thms ("zadd_ac", [zadd_assoc, zadd_commute, zadd_left_commute]);
 
 Goalw [int_of_def] "$# (m #+ n) = ($#m) $+ ($#n)";
 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
@@ -643,7 +643,7 @@
 qed "zmult_left_commute";
 
 (*Integer multiplication is an AC operator*)
-val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
+bind_thms ("zmult_ac", [zmult_assoc, zmult_commute, zmult_left_commute]);
 
 Goalw [int_def]
     "[| z1: int;  z2: int;  w: int |]  \
@@ -664,8 +664,8 @@
                                   zadd_zmult_distrib]) 1);
 qed "zadd_zmult_distrib2";
 
-val int_typechecks =
-    [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
+bind_thms ("int_typechecks",
+  [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type]);
 
 
 (*** Subtraction laws ***)
@@ -680,20 +680,13 @@
 qed "zminus_zdiff_eq";
 Addsimps [zminus_zdiff_eq];
 
-Goal "$- (z $- y) = y $- z";
-by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
-qed "zminus_zdiff_eq";
-Addsimps [zminus_zdiff_eq];
-
 Goalw [zdiff_def] "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)";
 by (stac zadd_zmult_distrib 1);
 by (simp_tac (simpset() addsimps [zmult_zminus]) 1);
 qed "zdiff_zmult_distrib";
 
-val zmult_commute'= inst "z" "w" zmult_commute;
-
 Goal "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)";
-by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1);
+by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute, zdiff_zmult_distrib]) 1);
 qed "zdiff_zmult_distrib2";
 
 Goal "x $+ (y $- z) = (x $+ y) $- z";