# HG changeset patch
# User wenzelm
# Date 968353969 -7200
# Node ID 473a6604da94ae9940f8f5bd92eced23e95b5dae
# Parent  5c027cca6262e6121c89260d3a0e8d4dccb72bc8
tuned ML code (the_context, bind_thms(s));

diff -r 5c027cca6262 -r 473a6604da94 src/ZF/AC.ML
--- a/src/ZF/AC.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/AC.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -7,7 +7,7 @@
 *)
 
 (*The same as AC, but no premise a:A*)
-val [nonempty] = goal AC.thy
+val [nonempty] = goal (the_context ())
      "[| !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)";
 by (excluded_middle_tac "A=0" 1);
 by (asm_simp_tac (simpset() addsimps [Pi_empty1]) 2 THEN Blast_tac 2);
@@ -28,7 +28,7 @@
 by (Blast_tac 1);
 qed "AC_Pi_Pow";
 
-val [nonempty] = goal AC.thy
+val [nonempty] = goal (the_context ())
      "[| !!x. x:A ==> (EX y. y:x)       \
 \     |] ==> EX f: A->Union(A). ALL x:A. f`x : x";
 by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Arith.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -15,7 +15,7 @@
 *)
 
 Addsimps [rec_type, nat_0_le];
-val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
+bind_thms ("nat_typechecks", [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat]);
 
 Goal "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
 by (etac rev_mp 1);
@@ -261,7 +261,7 @@
 qed "add_left_commute";
 
 (*Addition is an AC-operator*)
-val add_ac = [add_assoc, add_commute, add_left_commute];
+bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
 
 (*Cancellation law on the left*)
 Goal "[| raw_add(k, m) = raw_add(k, n);  k:nat |] ==> m=n";
@@ -496,6 +496,4 @@
 by (rtac (mult_commute RS subst_context) 1);
 qed "mult_left_commute";
 
-val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
-
-
+bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/ArithSimp.ML
--- a/src/ZF/ArithSimp.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/ArithSimp.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -75,10 +75,10 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self])));
 qed "div_termination";
 
-val div_rls =   (*for mod and div*)
+bind_thms ("div_rls",   (*for mod and div*)
     nat_typechecks @
     [Ord_transrec_type, apply_funtype, div_termination RS ltD,
-     nat_into_Ord, not_lt_iff_le RS iffD1];
+     nat_into_Ord, not_lt_iff_le RS iffD1]);
 
 val div_ss = simpset() addsimps [div_termination RS ltD,
 				 not_lt_iff_le RS iffD2];
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Bool.ML
--- a/src/ZF/Bool.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Bool.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -6,7 +6,7 @@
 Booleans in Zermelo-Fraenkel Set Theory 
 *)
 
-val bool_defs = [bool_def,cond_def];
+bind_thms ("bool_defs", [bool_def,cond_def]);
 
 Goalw [succ_def] "{0} = 1";
 by (rtac refl 1);
@@ -30,7 +30,7 @@
 qed "one_not_0";
 
 (** 1=0 ==> R **)
-val one_neq_0 = one_not_0 RS notE;
+bind_thm ("one_neq_0", one_not_0 RS notE);
 
 val major::prems = Goalw bool_defs
     "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P";
@@ -77,10 +77,19 @@
 
 fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)];
 
-val [not_1,not_0] = conds not_def;
-val [and_1,and_0] = conds and_def;
-val [or_1,or_0]   = conds or_def;
-val [xor_1,xor_0] = conds xor_def;
+val [not_1, not_0] = conds not_def;
+val [and_1, and_0] = conds and_def;
+val [or_1, or_0]   = conds or_def;
+val [xor_1, xor_0] = conds xor_def;
+
+bind_thm ("not_1", not_1);
+bind_thm ("not_0", not_0);
+bind_thm ("and_1", and_1);
+bind_thm ("and_0", and_0);
+bind_thm ("or_1", or_1);
+bind_thm ("or_0", or_0);
+bind_thm ("xor_1", xor_1);
+bind_thm ("xor_0", xor_0);
 
 Addsimps [not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
 
@@ -104,8 +113,8 @@
 
 AddTCs [xor_type];
 
-val bool_typechecks = [bool_1I, bool_0I, cond_type, not_type, and_type, 
-                       or_type, xor_type];
+bind_thms ("bool_typechecks",
+  [bool_1I, bool_0I, cond_type, not_type, and_type, or_type, xor_type]);
 
 (*** Laws for 'not' ***)
 
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Cardinal.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -17,7 +17,7 @@
 by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1));
 qed "decomp_bnd_mono";
 
-val [gfun] = goal Cardinal.thy
+val [gfun] = goal (the_context ())
     "g: Y->X ==>                                        \
 \    g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =       \
 \    X - lfp(X, %W. X - g``(Y - f``W)) ";
@@ -38,7 +38,7 @@
 by (REPEAT (ares_tac [fun_is_rel, image_subset, lfp_subset] 1));
 qed "decomposition";
 
-val prems = goal Cardinal.thy
+val prems = goal (the_context ())
     "[| f: inj(X,Y);  g: inj(Y,X) |] ==> EX h. h: bij(X,Y)";
 by (cut_facts_tac prems 1);
 by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1);
@@ -219,7 +219,7 @@
 qed "less_LeastE";
 
 (*Easier to apply than LeastI: conclusion has only one occurrence of P*)
-val prems = goal Cardinal.thy
+val prems = goal (the_context ())
     "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))";
 by (resolve_tac prems 1);
 by (rtac LeastI 1);
@@ -333,7 +333,7 @@
 by (blast_tac (claset() addSEs [ltE]) 1);
 qed "Card_0";
 
-val [premK,premL] = goal Cardinal.thy
+val [premK,premL] = goal (the_context ())
     "[| Card(K);  Card(L) |] ==> Card(K Un L)";
 by (rtac ([premK RS Card_is_Ord, premL RS Card_is_Ord] MRS Ord_linear_le) 1);
 by (asm_simp_tac 
@@ -780,7 +780,7 @@
 qed "nat_wf_on_converse_Memrel";
 
 Goal "n:nat ==> well_ord(n,converse(Memrel(n)))";
-by (forward_tac [transfer thy Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1);
+by (forward_tac [transfer (the_context ()) Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1);
 by (rewtac well_ord_def);
 by (blast_tac (claset() addSIs [tot_ord_converse, 
 			       nat_wf_on_converse_Memrel]) 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/CardinalArith.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -295,9 +295,9 @@
 qed "cmult_2";
 
 
-val sum_lepoll_prod = [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll,
+bind_thm ("sum_lepoll_prod", [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll,
         asm_rl, lepoll_refl] MRS (prod_lepoll_mono RSN (2, lepoll_trans))
-        |> standard;
+        |> standard);
 
 Goal "[| A lepoll B; 2 lepoll A |] ==> A+B lepoll A*B";
 by (REPEAT (ares_tac [[sum_lepoll_mono, sum_lepoll_prod]
@@ -791,8 +791,8 @@
 
 (** Theorems by Krzysztof Grabczewski, proofs by lcp **)
 
-val nat_implies_well_ord =
-  (transfer CardinalArith.thy nat_into_Ord) RS well_ord_Memrel;
+bind_thm ("nat_implies_well_ord",
+  (transfer (the_context ()) nat_into_Ord) RS well_ord_Memrel);
 
 Goal "[| m:nat; n:nat |] ==> m + n eqpoll m #+ n";
 by (rtac eqpoll_trans 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Cardinal_AC.ML
--- a/src/ZF/Cardinal_AC.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Cardinal_AC.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -15,7 +15,7 @@
 by (etac well_ord_cardinal_eqpoll 1);
 qed "cardinal_eqpoll";
 
-val cardinal_idem = cardinal_eqpoll RS cardinal_cong;
+bind_thm ("cardinal_idem", cardinal_eqpoll RS cardinal_cong);
 
 Goal "|X| = |Y| ==> X eqpoll Y";
 by (resolve_tac [AC_well_ord RS exE] 1);
@@ -160,7 +160,7 @@
 by (res_inst_tac [("x1", "f`x")] (UN_upper RSN (2,subset_trans)) 1);
 by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2);
 by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_rangeI]) 1);
-val inj_UN_subset = result();
+qed "inj_UN_subset";
 
 (*Simpler to require |W|=K; we'd have a bijection; but the theorem would
   be weaker.*)
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Epsilon.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -13,7 +13,7 @@
 by (rtac (nat_0I RS UN_upper) 1);
 qed "arg_subset_eclose";
 
-val arg_into_eclose = arg_subset_eclose RS subsetD;
+bind_thm ("arg_into_eclose", arg_subset_eclose RS subsetD);
 
 Goalw [eclose_def,Transset_def] "Transset(eclose(A))";
 by (rtac (subsetI RS ballI) 1);
@@ -32,8 +32,8 @@
 (* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
 bind_thm ("ecloseD", eclose_subset RS subsetD);
 
-val arg_in_eclose_sing = arg_subset_eclose RS singleton_subsetD;
-val arg_into_eclose_sing = arg_in_eclose_sing RS ecloseD;
+bind_thm ("arg_in_eclose_sing", arg_subset_eclose RS singleton_subsetD);
+bind_thm ("arg_into_eclose_sing", arg_in_eclose_sing RS ecloseD);
 
 (* This is epsilon-induction for eclose(A); see also eclose_induct_down...
    [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
@@ -112,11 +112,11 @@
 qed "under_Memrel";
 
 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
-val under_Memrel_eclose = Transset_eclose RS under_Memrel;
+bind_thm ("under_Memrel_eclose", Transset_eclose RS under_Memrel);
 
-val wfrec_ssubst = standard (wf_Memrel RS wfrec RS ssubst);
+bind_thm ("wfrec_ssubst", standard (wf_Memrel RS wfrec RS ssubst));
 
-val [kmemj,jmemi] = goal Epsilon.thy
+val [kmemj,jmemi] = goal (the_context ())
     "[| k:eclose({j});  j:eclose({i}) |] ==> \
 \    wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)";
 by (rtac (kmemj RS eclose_induct) 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Finite.ML
--- a/src/ZF/Finite.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Finite.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -19,7 +19,7 @@
 qed "Fin_mono";
 
 (* A : Fin(B) ==> A <= B *)
-val FinD = Fin.dom_subset RS subsetD RS PowD;
+bind_thm ("FinD", Fin.dom_subset RS subsetD RS PowD);
 
 (** Induction on finite sets **)
 
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Fixedpt.ML
--- a/src/ZF/Fixedpt.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Fixedpt.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -8,8 +8,6 @@
 Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
 *)
 
-open Fixedpt;
-
 (*** Monotone operators ***)
 
 val prems = Goalw [bnd_mono_def]
@@ -28,7 +26,7 @@
 by (Blast_tac 1);
 qed "bnd_monoD2";
 
-val [major,minor] = goal Fixedpt.thy
+val [major,minor] = goal (the_context ())
     "[| bnd_mono(D,h);  X<=D |] ==> h(X) <= D";
 by (rtac (major RS bnd_monoD2 RS subset_trans) 1);
 by (rtac (major RS bnd_monoD1) 3);
@@ -64,7 +62,7 @@
 qed "lfp_subset";
 
 (*Used in datatype package*)
-val [rew] = goal Fixedpt.thy "A==lfp(D,h) ==> A <= D";
+val [rew] = goal (the_context ()) "A==lfp(D,h) ==> A <= D";
 by (rewtac rew);
 by (rtac lfp_subset 1);
 qed "def_lfp_subset";
@@ -76,7 +74,7 @@
 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1));
 qed "lfp_greatest";
 
-val hmono::prems = goal Fixedpt.thy
+val hmono::prems = goal (the_context ())
     "[| bnd_mono(D,h);  h(A)<=A;  A<=D |] ==> h(lfp(D,h)) <= A";
 by (rtac (hmono RS bnd_monoD2 RS subset_trans) 1);
 by (rtac lfp_lowerbound 1);
@@ -89,7 +87,7 @@
 by (REPEAT (assume_tac 1));
 qed "lfp_lemma2";
 
-val [hmono] = goal Fixedpt.thy
+val [hmono] = goal (the_context ())
     "bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))";
 by (rtac lfp_lowerbound 1);
 by (rtac (hmono RS bnd_monoD2) 1);
@@ -103,7 +101,7 @@
 qed "lfp_Tarski";
 
 (*Definition form, to control unfolding*)
-val [rew,mono] = goal Fixedpt.thy
+val [rew,mono] = goal (the_context ())
     "[| A==lfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)";
 by (rewtac rew);
 by (rtac (mono RS lfp_Tarski) 1);
@@ -144,7 +142,7 @@
 
 (*This version is useful when "A" is not a subset of D;
   second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *)
-val [hsub,hmono] = goal Fixedpt.thy
+val [hsub,hmono] = goal (the_context ())
     "[| h(D Int A) <= A;  bnd_mono(D,h) |] ==> lfp(D,h) <= A";
 by (rtac (lfp_lowerbound RS subset_trans) 1);
 by (rtac (hmono RS bnd_mono_subset RS Int_greatest) 1);
@@ -189,7 +187,7 @@
 qed "gfp_subset";
 
 (*Used in datatype package*)
-val [rew] = goal Fixedpt.thy "A==gfp(D,h) ==> A <= D";
+val [rew] = goal (the_context ()) "A==gfp(D,h) ==> A <= D";
 by (rewtac rew);
 by (rtac gfp_subset 1);
 qed "def_gfp_subset";
@@ -200,7 +198,7 @@
 by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1);
 qed "gfp_least";
 
-val hmono::prems = goal Fixedpt.thy
+val hmono::prems = goal (the_context ())
     "[| bnd_mono(D,h);  A<=h(A);  A<=D |] ==> A <= h(gfp(D,h))";
 by (rtac (hmono RS bnd_monoD2 RSN (2,subset_trans)) 1);
 by (rtac gfp_subset 3);
@@ -214,7 +212,7 @@
 by (REPEAT (assume_tac 1));
 qed "gfp_lemma2";
 
-val [hmono] = goal Fixedpt.thy
+val [hmono] = goal (the_context ())
     "bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)";
 by (rtac gfp_upperbound 1);
 by (rtac (hmono RS bnd_monoD2) 1);
@@ -227,7 +225,7 @@
 qed "gfp_Tarski";
 
 (*Definition form, to control unfolding*)
-val [rew,mono] = goal Fixedpt.thy
+val [rew,mono] = goal (the_context ())
     "[| A==gfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)";
 by (rewtac rew);
 by (rtac (mono RS gfp_Tarski) 1);
@@ -241,7 +239,7 @@
 by (REPEAT (ares_tac [gfp_upperbound RS subsetD] 1));
 qed "weak_coinduct";
 
-val [subs_h,subs_D,mono] = goal Fixedpt.thy
+val [subs_h,subs_D,mono] = goal (the_context ())
     "[| X <= h(X Un gfp(D,h));  X <= D;  bnd_mono(D,h) |] ==>  \
 \    X Un gfp(D,h) <= h(X Un gfp(D,h))";
 by (rtac (subs_h RS Un_least) 1);
@@ -259,7 +257,7 @@
 qed "coinduct";
 
 (*Definition form, to control unfolding*)
-val rew::prems = goal Fixedpt.thy
+val rew::prems = goal (the_context ())
     "[| A == gfp(D,h);  bnd_mono(D,h);  a: X;  X <= h(X Un A);  X <= D |] ==> \
 \    a : A";
 by (rewtac rew);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/InfDatatype.ML
--- a/src/ZF/InfDatatype.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/InfDatatype.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -6,10 +6,10 @@
 Infinite-branching datatype definitions
 *)
 
-val fun_Limit_VfromE =
+bind_thm ("fun_Limit_VfromE",
    [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS
-     transfer InfDatatype.thy Limit_VfromE 
-   |> standard;
+     transfer (the_context ()) Limit_VfromE 
+   |> standard);
 
 Goal "[| f: D -> Vfrom(A,csucc(K));  |D| le K;  InfCard(K) |]  \
 \     ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)";
@@ -54,7 +54,7 @@
 qed "fun_in_Vcsucc";
 
 (*Remove <= from the rule above*)
-val fun_in_Vcsucc' = subsetI RSN (4, fun_in_Vcsucc);
+bind_thm ("fun_in_Vcsucc'", subsetI RSN (4, fun_in_Vcsucc));
 
 (** Version where K itself is the index set **)
 
@@ -93,8 +93,8 @@
           UN_upper RS subset_imp_lepoll RS lepoll_imp_Card_le);
 
 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
-val inf_datatype_intrs =  
+bind_thms ("inf_datatype_intrs",
     [InfCard_nat, InfCard_nat_Un_cardinal,
      Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc, 
      zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc,
-     Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ Data_Arg.intrs;
+     Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ Data_Arg.intrs);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Let.ML
--- a/src/ZF/Let.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Let.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -6,9 +6,7 @@
 Let expressions -- borrowed from HOL
 *)
 
-open Let;
-
-val [prem] = goalw thy
+val [prem] = goalw (the_context ())
     [Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))";
 by (rtac (refl RS prem) 1);
 qed "LetI";
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/List.ML
--- a/src/ZF/List.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/List.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -9,11 +9,11 @@
 (*** Aspects of the datatype definition ***)
 
 (*An elimination rule, for type-checking*)
-val ConsE = list.mk_cases "Cons(a,l) : list(A)";
+bind_thm ("ConsE", list.mk_cases "Cons(a,l) : list(A)");
 
 (*Proving freeness results*)
-val Cons_iff     = list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
-val Nil_Cons_iff = list.mk_free "~ Nil=Cons(a,l)";
+bind_thm ("Cons_iff", list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'");
+bind_thm ("Nil_Cons_iff", list.mk_free "~ Nil=Cons(a,l)");
 
 Goal "list(A) = {0} + (A * list(A))";
 let open list;  val rew = rewrite_rule con_defs in  
@@ -99,7 +99,7 @@
 
 (** map **)
 
-val prems = Goalw [get_def thy "map_list"] 
+val prems = Goalw [get_def (the_context ()) "map_list"] 
     "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
 by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
 qed "map_type";
@@ -111,21 +111,21 @@
 
 (** length **)
 
-Goalw [get_def thy "length_list"] 
+Goalw [get_def (the_context ()) "length_list"] 
     "l: list(A) ==> length(l) : nat";
 by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
 qed "length_type";
 
 (** app **)
 
-Goalw [get_def thy "op @_list"] 
+Goalw [get_def (the_context ()) "op @_list"] 
     "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
 by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
 qed "app_type";
 
 (** rev **)
 
-Goalw [get_def thy "rev_list"] 
+Goalw [get_def (the_context ()) "rev_list"] 
     "xs: list(A) ==> rev(xs) : list(A)";
 by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
 qed "rev_type";
@@ -133,7 +133,7 @@
 
 (** flat **)
 
-Goalw [get_def thy "flat_list"] 
+Goalw [get_def (the_context ()) "flat_list"] 
     "ls: list(list(A)) ==> flat(ls) : list(A)";
 by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
 qed "flat_type";
@@ -141,7 +141,7 @@
 
 (** set_of_list **)
 
-Goalw [get_def thy "set_of_list_list"] 
+Goalw [get_def (the_context ()) "set_of_list_list"] 
     "l: list(A) ==> set_of_list(l) : Pow(A)";
 by (etac list_rec_type 1);
 by (ALLGOALS (Blast_tac));
@@ -156,15 +156,15 @@
 
 (** list_add **)
 
-Goalw [get_def thy "list_add_list"] 
+Goalw [get_def (the_context ()) "list_add_list"] 
     "xs: list(nat) ==> list_add(xs) : nat";
 by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1));
 qed "list_add_type";
 
-val list_typechecks =
+bind_thms ("list_typechecks",
     list.intrs @
     [list_rec_type, map_type, map_type2, app_type, length_type, 
-     rev_type, flat_type, list_add_type];
+     rev_type, flat_type, list_add_type]);
 
 AddTCs list_typechecks;
 
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Nat.ML
--- a/src/ZF/Nat.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Nat.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -14,7 +14,7 @@
 qed "nat_bnd_mono";
 
 (* nat = {0} Un {succ(x). x:nat} *)
-val nat_unfold = nat_bnd_mono RS (nat_def RS def_lfp_Tarski);
+bind_thm ("nat_unfold", nat_bnd_mono RS (nat_def RS def_lfp_Tarski));
 
 (** Type checking of 0 and successor **)
 
@@ -44,7 +44,7 @@
 by (blast_tac (claset() addSEs [boolE]) 1);
 qed "bool_subset_nat";
 
-val bool_into_nat = bool_subset_nat RS subsetD;
+bind_thm ("bool_into_nat", bool_subset_nat RS subsetD);
 
 
 (** Injectivity properties and induction **)
@@ -97,7 +97,7 @@
 qed "Limit_nat";
 
 (* succ(i): nat ==> i: nat *)
-val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans;
+bind_thm ("succ_natD", [succI1, asm_rl, Ord_nat] MRS Ord_trans);
 AddSDs   [succ_natD];
 
 Goal "succ(n): nat <-> n: nat";
@@ -115,7 +115,7 @@
 qed "nat_le_Limit";
 
 (* [| succ(i): k;  k: nat |] ==> i: k *)
-val succ_in_naturalD = [succI1, asm_rl, nat_into_Ord] MRS Ord_trans;
+bind_thm ("succ_in_naturalD", [succI1, asm_rl, nat_into_Ord] MRS Ord_trans);
 
 Goal "[| m<n;  n: nat |] ==> m: nat";
 by (etac ltE 1);
@@ -131,7 +131,7 @@
 (** Variations on mathematical induction **)
 
 (*complete induction*)
-val complete_induct = Ord_nat RSN (2, Ord_induct);
+bind_thm ("complete_induct", Ord_nat RSN (2, Ord_induct));
 
 val prems = Goal
     "[| m: nat;  n: nat;  \
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/OrdQuant.ML
--- a/src/ZF/OrdQuant.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/OrdQuant.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      ZF/AC/OrdQuant.thy
+(*  Title:      ZF/OrdQuant.ML
     ID:         $Id$
     Authors:    Krzysztof Grabczewski and L C Paulson
 
@@ -97,8 +97,7 @@
 AddSEs [oexE, OUN_E];
 AddEs  [rev_oallE];
 
-val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, 
-                           ZF_mem_pairs);
+val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
 
 simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
                         addsimps [oall_simp, ltD RS beta]
@@ -111,4 +110,3 @@
 by (etac Ord_induct 1 THEN assume_tac 1);
 by (fast_tac (claset() addIs prems) 1);
 qed "lt_induct";
-
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/OrderArith.ML
--- a/src/ZF/OrderArith.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/OrderArith.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -182,7 +182,7 @@
 
 (** Linearity **)
 
-val [lina,linb] = goal OrderArith.thy
+val [lina,linb] = goal (the_context ())
     "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))";
 by (rewtac linear_def);    (*Note! the premises are NOT rewritten*)
 by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac SigmaE));
@@ -354,7 +354,7 @@
 
 (** Linearity **)
 
-val [finj,lin] = goalw OrderArith.thy [inj_def]
+val [finj,lin] = goalw (the_context ()) [inj_def]
     "[| f: inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))";
 by (rewtac linear_def);    (*Note! the premises are NOT rewritten*)
 by (REPEAT_FIRST (ares_tac [ballI]));
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/OrderType.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -12,7 +12,7 @@
 
 (**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
 
-val [prem] = goal OrderType.thy "j le i ==> well_ord(j, Memrel(i))";
+val [prem] = goal (the_context ()) "j le i ==> well_ord(j, Memrel(i))";
 by (rtac well_ordI 1);
 by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
 by (resolve_tac [prem RS ltE] 1);
@@ -87,7 +87,7 @@
 qed "ordermap_pred_unfold";
 
 (*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
-val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
+bind_thm ("ordermap_unfold", rewrite_rule [pred_def] ordermap_pred_unfold);
 
 (*** Showing that ordermap, ordertype yield ordinals ***)
 
@@ -614,7 +614,7 @@
 by (asm_simp_tac (simpset() addsimps [oadd_odiff_inverse, oadd_le_self]) 1);
 qed "odiff_oadd_inverse";
 
-val [i_lt_j, k_le_i] = goal OrderType.thy
+val [i_lt_j, k_le_i] = goal (the_context ())
     "[| i<j;  k le i |] ==> i--k < j--k";
 by (rtac (k_le_i RS lt_Ord RSN (2,oadd_lt_cancel2)) 1);
 by (simp_tac
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Ordinal.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      ZF/Ordinal.thy
+(*  Title:      ZF/Ordinal.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -25,19 +25,19 @@
 by (Blast_tac 1);
 qed "Transset_doubleton_D";
 
-val [prem1,prem2] = goalw Ordinal.thy [Pair_def]
+val [prem1,prem2] = goalw (the_context ()) [Pair_def]
     "[| Transset(C); <a,b>: C |] ==> a:C & b: C";
 by (cut_facts_tac [prem2] 1);   
 by (blast_tac (claset() addSDs [prem1 RS Transset_doubleton_D]) 1);
 qed "Transset_Pair_D";
 
-val prem1::prems = goal Ordinal.thy
+val prem1::prems = goal (the_context ())
     "[| Transset(C); A*B <= C; b: B |] ==> A <= C";
 by (cut_facts_tac prems 1);
 by (blast_tac (claset() addSDs [prem1 RS Transset_Pair_D]) 1);
 qed "Transset_includes_domain";
 
-val prem1::prems = goal Ordinal.thy
+val prem1::prems = goal (the_context ())
     "[| Transset(C); A*B <= C; a: A |] ==> B <= C";
 by (cut_facts_tac prems 1);
 by (blast_tac (claset() addSDs [prem1 RS Transset_Pair_D]) 1);
@@ -105,7 +105,7 @@
 qed "Ord_in_Ord";
 
 (* Ord(succ(j)) ==> Ord(j) *)
-val Ord_succD = succI1 RSN (2, Ord_in_Ord);
+bind_thm ("Ord_succD", succI1 RSN (2, Ord_in_Ord));
 
 AddSDs [Ord_succD];
 
@@ -235,7 +235,7 @@
 (* [| i<j;  ~P ==> j<i |] ==> P *)
 bind_thm ("lt_asym", lt_not_sym RS swap);
 
-val [major]= goal Ordinal.thy "i<i ==> P";
+val [major]= goal (the_context ()) "i<i ==> P";
 by (rtac (major RS (major RS lt_asym)) 1) ;
 qed "lt_irrefl";
 
@@ -261,7 +261,7 @@
 by (asm_simp_tac (simpset() addsimps [le_iff]) 1);
 qed "le_eqI";
 
-val le_refl = refl RS le_eqI;
+bind_thm ("le_refl", refl RS le_eqI);
 
 Goal "i le i <-> Ord(i)";
 by (asm_simp_tac (simpset() addsimps [lt_not_refl, le_iff]) 1);
@@ -381,7 +381,7 @@
 qed "Transset_induct";
 
 (*Induction over an ordinal*)
-val Ord_induct = Ord_is_Transset RSN (2, Transset_induct);
+bind_thm ("Ord_induct", Ord_is_Transset RSN (2, Transset_induct));
 
 (*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
 val [major,indhyp] = Goal
@@ -584,7 +584,7 @@
 by (REPEAT_SOME assume_tac);
 qed "Un_least_lt_iff";
 
-val [ordi,ordj,ordk] = goal Ordinal.thy
+val [ordi,ordj,ordk] = goal (the_context ())
     "[| Ord(i); Ord(j); Ord(k) |] ==> i Un j : k  <->  i:k & j:k";
 by (cut_inst_tac [("k","k")] ([ordi,ordj] MRS Un_least_lt_iff) 1);
 by (asm_full_simp_tac (simpset() addsimps [lt_def,ordi,ordj,ordk]) 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Perm.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -62,7 +62,7 @@
 
 Goalw [inj_def] "[| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b";
 by (Blast_tac 1);
-val inj_apply_equality = result();
+qed "inj_apply_equality";
 
 (** A function with a left inverse is an injection **)
 
@@ -143,7 +143,7 @@
 by (Simp_tac 1);
 qed "id_subset_inj";
 
-val id_inj = subset_refl RS id_subset_inj;
+bind_thm ("id_inj", subset_refl RS id_subset_inj);
 
 Goalw [id_def,surj_def] "id(A): surj(A,A)";
 by (blast_tac (claset() addIs [lam_type, beta]) 1);
@@ -180,7 +180,7 @@
 			       inj_is_fun]) 1);
 qed "left_inverse";
 
-val left_inverse_bij = bij_is_inj RS left_inverse;
+bind_thm ("left_inverse_bij", bij_is_inj RS left_inverse);
 
 Goal "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b";
 by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);
@@ -421,7 +421,7 @@
 (*right inverse of composition; one inclusion is
                 f: A->B ==> f O converse(f) <= id(B) 
 *)
-val [prem] = goalw Perm.thy [surj_def]
+val [prem] = goalw (the_context ()) [surj_def]
     "f: surj(A,B) ==> f O converse(f) = id(B)";
 val appfD = (prem RS CollectD1) RSN (3,apply_equality2);
 by (cut_facts_tac [prem] 1);
@@ -489,7 +489,7 @@
 
 (** Restrictions as surjections and bijections *)
 
-val prems = goalw Perm.thy [surj_def]
+val prems = goalw (the_context ()) [surj_def]
     "f: Pi(A,B) ==> f: surj(A, f``A)";
 val rls = apply_equality :: (prems RL [apply_Pair,Pi_type]);
 by (fast_tac (claset() addIs rls) 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/QPair.ML
--- a/src/ZF/QPair.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/QPair.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -62,10 +62,10 @@
 
 (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
 
-val QSigmaE2 = 
+bind_thm ("QSigmaE2",
   rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
                   THEN prune_params_tac)
-      (inst "c" "<a;b>" QSigmaE);  
+      (inst "c" "<a;b>" QSigmaE));
 
 AddSEs [QSigmaE2, QSigmaE];
 
@@ -205,7 +205,7 @@
 
 (**** The Quine-inspired notion of disjoint sum ****)
 
-val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def];
+bind_thms ("qsum_defs", [qsum_def,QInl_def,QInr_def,qcase_def]);
 
 (** Introduction rules for the injections **)
 
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/QUniv.ML
--- a/src/ZF/QUniv.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/QUniv.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -63,7 +63,7 @@
 bind_thm ("A_subset_quniv",
           [A_subset_univ, univ_subset_quniv] MRS subset_trans);
 
-val A_into_quniv = A_subset_quniv RS subsetD;
+bind_thm ("A_into_quniv", A_subset_quniv RS subsetD);
 
 (*** univ(A) closure for Quine-inspired pairs and injections ***)
 
@@ -79,12 +79,12 @@
 by (etac (empty_subsetI RS QPair_subset_univ) 1);
 qed "QInl_subset_univ";
 
-val naturals_subset_nat =
+bind_thm ("naturals_subset_nat",
     rewrite_rule [Transset_def] (Ord_nat RS Ord_is_Transset)
-    RS bspec;
+    RS bspec);
 
-val naturals_subset_univ = 
-    [naturals_subset_nat, nat_subset_univ] MRS subset_trans;
+bind_thm ("naturals_subset_univ",
+    [naturals_subset_nat, nat_subset_univ] MRS subset_trans);
 
 Goalw [QInr_def] "a <= univ(A) ==> QInr(a) <= univ(A)";
 by (etac (nat_1I RS naturals_subset_univ RS QPair_subset_univ) 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Rel.ML
--- a/src/ZF/Rel.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Rel.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -6,8 +6,6 @@
 Relations in Zermelo-Fraenkel Set Theory 
 *)
 
-open Rel;
-
 (*** Some properties of relations -- useful? ***)
 
 (* irreflexivity *)
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Sum.ML
--- a/src/ZF/Sum.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Sum.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -18,7 +18,7 @@
 by (Blast_tac 1);
 qed "Part_eqI";
 
-val PartI = refl RSN (2,Part_eqI);
+bind_thm ("PartI", refl RSN (2,Part_eqI));
 
 val major::prems = Goalw [Part_def]
     "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
@@ -38,7 +38,7 @@
 
 (*** Rules for Disjoint Sums ***)
 
-val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
+bind_thms ("sum_defs", [sum_def,Inl_def,Inr_def,case_def]);
 
 Goalw (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)";
 by (Blast_tac 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Trancl.ML
--- a/src/ZF/Trancl.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Trancl.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -19,7 +19,7 @@
 qed "rtrancl_mono";
 
 (* r^* = id(field(r)) Un ( r O r^* )    *)
-val rtrancl_unfold = rtrancl_bnd_mono RS (rtrancl_def RS def_lfp_Tarski);
+bind_thm ("rtrancl_unfold", rtrancl_bnd_mono RS (rtrancl_def RS def_lfp_Tarski));
 
 (** The relation rtrancl **)
 
@@ -138,7 +138,7 @@
 qed "rtrancl_into_trancl1";
 
 (*intro rule from r and r^*  *)
-val prems = goal Trancl.thy
+val prems = goal (the_context ())
     "[| <a,b> : r;  <b,c> : r^* |]   ==>  <a,c> : r^+";
 by (resolve_tac (prems RL [rtrancl_induct]) 1);
 by (resolve_tac (prems RL [r_into_trancl]) 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Univ.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -156,7 +156,7 @@
 by (Blast_tac 1);
 qed "Vfrom_Union";
 
-val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
+val [prem] = goal (the_context ()) "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
 by (stac Vfrom 1);
 by (rtac equalityI 1);
 (*first inclusion*)
@@ -180,7 +180,7 @@
 
 (*NB. limit ordinals are non-empty;
                         Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
-val [limiti] = goal Univ.thy
+val [limiti] = goal (the_context ())
     "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
 by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1);
 by (stac (limiti RS Limit_Union_eq) 1);
@@ -201,9 +201,9 @@
 by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
 qed "Limit_VfromE";
 
-val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom;
+bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom);
 
-val [major,limiti] = goal Univ.thy
+val [major,limiti] = goal (the_context ())
     "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)";
 by (rtac ([major,limiti] MRS Limit_VfromE) 1);
 by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
@@ -214,7 +214,7 @@
 bind_thm ("Vfrom_UnI2", Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD));
 
 (*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
-val [aprem,bprem,limiti] = goal Univ.thy
+val [aprem,bprem,limiti] = goal (the_context ())
     "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
 \    {a,b} : Vfrom(A,i)";
 by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
@@ -225,7 +225,7 @@
 by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
 qed "doubleton_in_VLimit";
 
-val [aprem,bprem,limiti] = goal Univ.thy
+val [aprem,bprem,limiti] = goal (the_context ())
     "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
 \    <a,b> : Vfrom(A,i)";
 (*Infer that a, b occur at ordinals x,xa < i.*)
@@ -340,7 +340,7 @@
 by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
 qed "prod_in_Vfrom";
 
-val [aprem,bprem,limiti,transset] = goal Univ.thy
+val [aprem,bprem,limiti,transset] = goal (the_context ())
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
 \  a*b : Vfrom(A,i)";
 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
@@ -360,7 +360,7 @@
                            i_subset_Vfrom RS subsetD]) 1);
 qed "sum_in_Vfrom";
 
-val [aprem,bprem,limiti,transset] = goal Univ.thy
+val [aprem,bprem,limiti,transset] = goal (the_context ())
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
 \  a+b : Vfrom(A,i)";
 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
@@ -385,7 +385,7 @@
 by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
 qed "fun_in_Vfrom";
 
-val [aprem,bprem,limiti,transset] = goal Univ.thy
+val [aprem,bprem,limiti,transset] = goal (the_context ())
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
 \  a->b : Vfrom(A,i)";
 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
@@ -415,9 +415,9 @@
 by (Blast_tac 1);
 qed "Vset";
 
-val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
+bind_thm ("Vset_succ", Transset_0 RS Transset_Vfrom_succ);
 
-val Transset_Vset = Transset_0 RS Transset_Vfrom;
+bind_thm ("Transset_Vset", Transset_0 RS Transset_Vfrom);
 
 (** Characterisation of the elements of Vset(i) **)
 
@@ -495,8 +495,8 @@
 by (rtac rank_pair2 1);
 qed "rank_Inr";
 
-val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2];
-val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans]));
+bind_thms ("rank_rls", [rank_Inl, rank_Inr, rank_pair1, rank_pair2]);
+bind_thms ("rank_trans_rls", rank_rls @ (rank_rls RLN (2, [lt_trans])));
 
 val rank_ss = simpset() addsimps [VsetI] addsimps rank_trans_rls;
 
@@ -586,7 +586,7 @@
 by (rtac A_subset_Vfrom 1);
 qed "A_subset_univ";
 
-val A_into_univ = A_subset_univ RS subsetD;
+bind_thm ("A_into_univ", A_subset_univ RS subsetD);
 
 (** Closure under unordered and ordered pairs **)
 
@@ -669,7 +669,7 @@
 by (etac Limit_VfromE 1);
 by (assume_tac 1);
 by (blast_tac (claset() addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
-val Fin_Vfrom_lemma = result();
+qed "Fin_Vfrom_lemma";
 
 Goal "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
 by (rtac subsetI 1);
@@ -677,13 +677,13 @@
 by Safe_tac;
 by (resolve_tac [Vfrom RS ssubst] 1);
 by (blast_tac (claset() addSDs [ltD]) 1);
-val Fin_VLimit = result();
+qed "Fin_VLimit";
 
 bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans);
 
 Goalw [univ_def] "Fin(univ(A)) <= univ(A)";
 by (rtac (Limit_nat RS Fin_VLimit) 1);
-val Fin_univ = result();
+qed "Fin_univ";
 
 (** Closure under finite powers (functions from a fixed natural number) **)
 
@@ -691,13 +691,13 @@
 by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
 by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
                       nat_subset_VLimit, subset_refl] 1));
-val nat_fun_VLimit = result();
+qed "nat_fun_VLimit";
 
 bind_thm ("nat_fun_subset_VLimit", [Pi_mono, nat_fun_VLimit] MRS subset_trans);
 
 Goalw [univ_def] "n: nat ==> n -> univ(A) <= univ(A)";
 by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
-val nat_fun_univ = result();
+qed "nat_fun_univ";
 
 
 (** Closure under finite function space **)
@@ -706,30 +706,30 @@
 Goal "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)";
 by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1);
 by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1));
-val FiniteFun_VLimit1 = result();
+qed "FiniteFun_VLimit1";
 
 Goalw [univ_def] "univ(A) -||> univ(A) <= univ(A)";
 by (rtac (Limit_nat RS FiniteFun_VLimit1) 1);
-val FiniteFun_univ1 = result();
+qed "FiniteFun_univ1";
 
 (*Version for a fixed domain*)
 Goal "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)";
 by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1);
 by (etac FiniteFun_VLimit1 1);
-val FiniteFun_VLimit = result();
+qed "FiniteFun_VLimit";
 
 Goalw [univ_def]
     "W <= univ(A) ==> W -||> univ(A) <= univ(A)";
 by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1);
-val FiniteFun_univ = result();
+qed "FiniteFun_univ";
 
 Goal "[| f: W -||> univ(A);  W <= univ(A) |] ==> f : univ(A)";
 by (eresolve_tac [FiniteFun_univ RS subsetD] 1);
 by (assume_tac 1);
-val FiniteFun_in_univ = result();
+qed "FiniteFun_in_univ";
 
 (*Remove <= from the rule above*)
-val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ);
+bind_thm ("FiniteFun_in_univ'", subsetI RSN (2, FiniteFun_in_univ));
 
 
 (**** For QUniv.  Properties of Vfrom analogous to the "take-lemma" ****)
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Update.ML
--- a/src/ZF/Update.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Update.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      ZF/Update.thy
+(*  Title:      ZF/Update.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
@@ -6,8 +6,6 @@
 Function updates: like theory Map, but for ordinary functions
 *)
 
-open Update;
-
 Goal "f(x:=y) ` z = (if z=x then y else f`z)";
 by (simp_tac (simpset() addsimps [update_def]) 1);
 by (case_tac "z : domain(f)" 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/WF.ML
--- a/src/ZF/WF.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/WF.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      ZF/wf.ML
+(*  Title:      ZF/WF.ML
     ID:         $Id$
     Author:     Tobias Nipkow and Lawrence C Paulson
     Copyright   1998  University of Cambridge
@@ -175,7 +175,7 @@
 val bchain_tac = EVERY' [rtac (bspec RS mp), assume_tac, assume_tac ];
 
 (*transitive closure of a WF relation is WF provided A is downwards closed*)
-val [wfr,subs] = goal WF.thy
+val [wfr,subs] = goal (the_context ())
     "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)";
 by (rtac wf_onI2 1);
 by (bchain_tac 1);
@@ -206,7 +206,7 @@
 by (assume_tac 1);
 qed "is_recfun_type";
 
-val [isrec,rel] = goalw WF.thy [is_recfun_def]
+val [isrec,rel] = goalw (the_context ()) [is_recfun_def]
     "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";
 by (res_inst_tac [("P", "%x.?t(x) = (?u::i)")] (isrec RS ssubst) 1);
 by (rtac (rel RS underI RS beta) 1);
@@ -232,7 +232,7 @@
 by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
 qed_spec_mp "is_recfun_equal";
 
-val prems as [wfr,transr,recf,recg,_] = goal WF.thy
+val prems as [wfr,transr,recf,recg,_] = goal (the_context ())
     "[| wf(r);  trans(r);       \
 \       is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |] ==> \
 \    restrict(f, r-``{b}) = g";
@@ -296,7 +296,7 @@
 (** Removal of the premise trans(r) **)
 
 (*NOT SUITABLE FOR REWRITING: it is recursive!*)
-val [wfr] = goalw WF.thy [wfrec_def]
+val [wfr] = goalw (the_context ()) [wfrec_def]
     "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
 by (stac (wfr RS wf_trancl RS wftrec) 1);
 by (rtac trans_trancl 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/ZF.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -10,7 +10,7 @@
 Goal "[| b:A;  a=b |] ==> a:A";
 by (etac ssubst 1);
 by (assume_tac 1);
-val subst_elem = result();
+qed "subst_elem";
 
 
 (*** Bounded universal quantifier ***)
@@ -505,50 +505,28 @@
 by (best_tac cantor_cs 1);
 qed "cantor";
 
-(*Lemma for the inductive definition in Zorn.thy*)
+(*Lemma for the inductive definition in theory Zorn*)
 Goal "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)";
 by (Blast_tac 1);
 qed "Union_in_Pow";
 
 
+(* update rulify setup -- include bounded All *)
+
+Goal "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))";
+by (simp_tac (simpset () addsimps (Ball_def :: thms "atomize")) 1);
+qed "ball_eq";
+
 local
-val (bspecT, bspec') = make_new_spec bspec
+  val ss = FOL_basic_ss addsimps
+    (Drule.norm_hhf_eq :: map Thm.symmetric (ball_eq :: thms "atomize"));
 in
 
-fun RSbspec th =
-  (case concl_of th of
-     _ $ (Const("Ball",_) $ _ $ Abs(a,_,_)) =>
-         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),bspecT))
-         in th RS forall_elim ca bspec' end
-  | _ => raise THM("RSbspec",0,[th]));
-
-val normalize_thm_ZF = normalize_thm [RSspec,RSbspec,RSmp];
+structure Rulify = RulifyFun
+ (val make_meta = Simplifier.simplify ss
+  val full_make_meta = Simplifier.full_simplify ss);
 
-fun qed_spec_mp name =
-  let val thm = normalize_thm_ZF (result())
-  in bind_thm(name, thm) end;
-
-fun qed_goal_spec_mp name thy s p = 
-      bind_thm (name, normalize_thm_ZF (prove_goal thy s p));
-
-fun qed_goalw_spec_mp name thy defs s p = 
-      bind_thm (name, normalize_thm_ZF (prove_goalw thy defs s p));
+structure BasicRulify: BASIC_RULIFY = Rulify;
+open BasicRulify;
 
 end;
-
-
-(* attributes *)
-
-local
-
-fun gen_rulify x = 
-    Attrib.no_args (Drule.rule_attribute (K (normalize_thm_ZF))) x;
-
-in
-
-val attrib_setup =
- [Attrib.add_attributes
-  [("rulify", (gen_rulify, gen_rulify), 
-    "put theorem into standard rule form")]];
-
-end;
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Zorn.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -33,9 +33,11 @@
 
 (*Introduction rules*)
 val [TFin_nextI, Pow_TFin_UnionI] = TFin.intrs;
-val TFin_UnionI = PowI RS Pow_TFin_UnionI;
+bind_thm ("TFin_nextI", TFin_nextI);
+bind_thm ("Pow_TFin_UnionI", Pow_TFin_UnionI);
+bind_thm ("TFin_UnionI", PowI RS Pow_TFin_UnionI);
 
-val TFin_is_subset = TFin.dom_subset RS subsetD RS PowD;
+bind_thm ("TFin_is_subset", TFin.dom_subset RS subsetD RS PowD);
 
 
 (** Structural induction on TFin(S,next) **)
@@ -66,7 +68,7 @@
 
 (*Lemma 2 of section 3.2.  Interesting in its own right!
   Requires next: increasing(S) in the second induction step. *)
-val [major,ninc] = goal Zorn.thy
+val [major,ninc] = goal (the_context ())
     "[| m: TFin(S,next);  next: increasing(S) \
 \    |] ==> ALL n: TFin(S,next) . n<=m --> n=m | next`n<=m";
 by (rtac (major RS TFin_induct) 1);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/equalities.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -29,7 +29,7 @@
 Goal "[| a: C;  ALL y:C. y=b |] ==> C = {b}";
 by (Blast_tac 1);
 qed "equal_singleton_lemma";
-val equal_singleton = ballI RSN (2,equal_singleton_lemma);
+bind_thm ("equal_singleton", ballI RSN (2,equal_singleton_lemma));
 
 
 (** Binary Intersection **)
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/func.ML
--- a/src/ZF/func.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/func.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -364,9 +364,9 @@
 
 (** The Union of 2 disjoint functions is a function **)
 
-val Un_rls = [Un_subset_iff, SUM_Un_distrib1, prod_Un_distrib2, 
+bind_thms ("Un_rls", [Un_subset_iff, SUM_Un_distrib1, prod_Un_distrib2, 
               Un_upper1 RSN (2, subset_trans), 
-              Un_upper2 RSN (2, subset_trans)];
+              Un_upper2 RSN (2, subset_trans)]);
 
 Goal "[| f: A->B;  g: C->D;  A Int C = 0  |]  \
 \                 ==> (f Un g) : (A Un C) -> (B Un D)";
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/mono.ML
--- a/src/ZF/mono.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/mono.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -58,7 +58,7 @@
 Goal "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)";
 by (Blast_tac 1);
 qed "Sigma_mono_lemma";
-val Sigma_mono = ballI RSN (2,Sigma_mono_lemma);
+bind_thm ("Sigma_mono", ballI RSN (2,Sigma_mono_lemma));
 
 Goalw sum_defs "[| A<=C;  B<=D |] ==> A+B <= C+D";
 by (REPEAT (ares_tac [subset_refl,Un_mono,Sigma_mono] 1));
@@ -83,7 +83,7 @@
 \                          QSigma(A,B) <= QSigma(C,D)";
 by (Blast_tac 1);
 qed "QSigma_mono_lemma";
-val QSigma_mono = ballI RSN (2,QSigma_mono_lemma);
+bind_thm ("QSigma_mono", ballI RSN (2,QSigma_mono_lemma));
 
 Goalw [QInl_def] "a<=b ==> QInl(a) <= QInl(b)";
 by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
@@ -187,6 +187,5 @@
 qed "all_mono";
 
 (*Used in intr_elim.ML and in individual datatype definitions*)
-val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
-                   ex_mono, Collect_mono, Part_mono, in_mono];
-
+bind_thms ("basic_monos",
+  [subset_refl, imp_refl, disj_mono, conj_mono, ex_mono, Collect_mono, Part_mono, in_mono]);
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/simpdata.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -63,6 +63,13 @@
 
 end;
 
+bind_thms ("ball_simps", ball_simps);
+bind_thm ("ball_conj_distrib", ball_conj_distrib);
+bind_thms ("bex_simps", bex_simps);
+bind_thm ("bex_disj_distrib", bex_disj_distrib);
+bind_thms ("Rep_simps", Rep_simps);
+bind_thms ("misc_simps", misc_simps);
+
 Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
 
 
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/subset.ML
--- a/src/ZF/subset.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/subset.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -196,11 +196,11 @@
 by (blast_tac (claset() addIs prems) 1);
 qed "RepFun_subset";
 
-val subset_SIs =
+bind_thms ("subset_SIs",
     [subset_refl, cons_subsetI, subset_consI, 
      Union_least, UN_least, Un_least, 
      Inter_greatest, Int_greatest, RepFun_subset,
-     Un_upper1, Un_upper2, Int_lower1, Int_lower2];
+     Un_upper1, Un_upper2, Int_lower1, Int_lower2]);
 
 
 (*A claset for subset reasoning*)
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/upair.ML
--- a/src/ZF/upair.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/upair.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -14,8 +14,8 @@
 
 (*** Lemmas about power sets  ***)
 
-val Pow_bottom = empty_subsetI RS PowI;         (* 0 : Pow(B) *)
-val Pow_top = subset_refl RS PowI;              (* A : Pow(A) *)
+bind_thm ("Pow_bottom", empty_subsetI RS PowI);         (* 0 : Pow(B) *)
+bind_thm ("Pow_top", subset_refl RS PowI);              (* A : Pow(A) *)
 
 
 (*** Unordered pairs - Upair ***)
@@ -303,8 +303,7 @@
 bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if);
 bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if);
 
-val split_ifs = [split_if_eq1, split_if_eq2,
-		 split_if_mem1, split_if_mem2];
+bind_thms ("split_ifs", [split_if_eq1, split_if_eq2, split_if_mem1, split_if_mem2]);
 
 (*Logically equivalent to split_if_mem2*)
 Goal "a: (if P then x else y) <-> P & a:x | ~P & a:y";
@@ -387,7 +386,7 @@
 
 
 (* succ(c) <= B ==> c : B *)
-val succ_subsetD = succI1 RSN (2,subsetD);
+bind_thm ("succ_subsetD", succI1 RSN (2,subsetD));
 
 (* succ(b) ~= b *)
 bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
@@ -403,4 +402,3 @@
 
 (*Not needed now that cons is available.  Deletion reduces the search space.*)
 Delrules [UpairI1,UpairI2,UpairE];
-
diff -r 5c027cca6262 -r 473a6604da94 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/upair.thy	Thu Sep 07 21:12:49 2000 +0200
@@ -2,15 +2,12 @@
     ID:         $Id$
     Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
     Copyright   1993  University of Cambridge
-
-Dummy theory, but holds the standard ZF simpset.
 *)
 
 theory upair = ZF
 files "Tools/typechk":
 
-setup
-  TypeCheck.setup
+setup TypeCheck.setup
+setup Rulify.setup
 
 end
-