# HG changeset patch
# User clasohm
# Date 787400238 -3600
# Node ID c533bc92e8825f940988f819c1b028afc90c37d1
# Parent  4d0545e93c0dbdb55356fe50b904f0e2b3cac12e
added bind_thm for theorems made by "standard ..."

diff -r 4d0545e93c0d -r c533bc92e882 Arith.ML
--- a/Arith.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/Arith.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -189,7 +189,7 @@
 qed "diffs0_imp_equal_lemma";
 
 (*  [| m-n = 0;  n-m = 0 |] ==> m=n  *)
-val diffs0_imp_equal = standard (diffs0_imp_equal_lemma RS mp RS mp);
+bind_thm ("diffs0_imp_equal", (diffs0_imp_equal_lemma RS mp RS mp));
 
 val [prem] = goal Arith.thy "m<n ==> 0<n-m";
 by (rtac (prem RS rev_mp) 1);
@@ -235,8 +235,8 @@
 by (rtac le_add2 1);
 qed "le_add1";
 
-val less_add_Suc1 = standard (lessI RS (le_add1 RS le_less_trans));
-val less_add_Suc2 = standard (lessI RS (le_add2 RS le_less_trans));
+bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
+bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
 
 goal Arith.thy "m+k<=n --> m<=(n::nat)";
 by (nat_ind_tac "k" 1);
diff -r 4d0545e93c0d -r c533bc92e882 HOL.ML
--- a/HOL.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/HOL.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -16,7 +16,7 @@
  (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
 
 (*calling "standard" reduces maxidx to 0*)
-val ssubst = standard (sym RS subst);
+bind_thm ("ssubst", (sym RS subst));
 
 qed_goal "trans" HOL.thy "[| r=s; s=t |] ==> r=t"
  (fn prems =>
diff -r 4d0545e93c0d -r c533bc92e882 List.ML
--- a/List.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/List.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -10,10 +10,10 @@
 
 val [Nil_not_Cons,Cons_not_Nil] = list.distinct;
 
-bind_thm("Cons_neq_Nil", standard (Cons_not_Nil RS notE));
+bind_thm("Cons_neq_Nil", Cons_not_Nil RS notE);
 bind_thm("Nil_neq_Cons", sym RS Cons_neq_Nil);
 
-bind_thm("Cons_inject", standard ((hd list.inject) RS iffD1 RS conjE));
+bind_thm("Cons_inject", (hd list.inject) RS iffD1 RS conjE);
 
 val list_ss = HOL_ss addsimps list.simps;
 
diff -r 4d0545e93c0d -r c533bc92e882 Nat.ML
--- a/Nat.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/Nat.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -95,9 +95,9 @@
 by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
 qed "Suc_not_Zero";
 
-val Zero_not_Suc = standard (Suc_not_Zero RS not_sym);
+bind_thm ("Zero_not_Suc", (Suc_not_Zero RS not_sym));
 
-val Suc_neq_Zero = standard (Suc_not_Zero RS notE);
+bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
 val Zero_neq_Suc = sym RS Suc_neq_Zero;
 
 (** Injectiveness of Suc **)
@@ -158,7 +158,7 @@
 
 (*** nat_rec -- by wf recursion on pred_nat ***)
 
-val nat_rec_unfold = standard (wf_pred_nat RS (nat_rec_def RS def_wfrec));
+bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec)));
 
 (** conversion rules **)
 
@@ -221,7 +221,7 @@
 qed "less_not_sym";
 
 (* [| n<m; m<n |] ==> R *)
-val less_asym = standard (less_not_sym RS notE);
+bind_thm ("less_asym", (less_not_sym RS notE));
 
 goalw Nat.thy [less_def] "~ n<(n::nat)";
 by (rtac notI 1);
@@ -229,7 +229,7 @@
 qed "less_not_refl";
 
 (* n<n ==> R *)
-val less_anti_refl = standard (less_not_refl RS notE);
+bind_thm ("less_anti_refl", (less_not_refl RS notE));
 
 goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
 by(fast_tac (HOL_cs addEs [less_anti_refl]) 1);
@@ -252,7 +252,7 @@
 qed "not_less0";
 
 (* n<0 ==> R *)
-val less_zeroE = standard (not_less0 RS notE);
+bind_thm ("less_zeroE", (not_less0 RS notE));
 
 val [major,less,eq] = goal Nat.thy
     "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";
diff -r 4d0545e93c0d -r c533bc92e882 Subst/UTerm.ML
--- a/Subst/UTerm.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/Subst/UTerm.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -32,7 +32,7 @@
 qed "uterm_sexp";
 
 (* A <= sexp ==> uterm(A) <= sexp *)
-val uterm_subset_sexp = standard ([uterm_mono, uterm_sexp] MRS subset_trans);
+bind_thm ("uterm_subset_sexp", ([uterm_mono, uterm_sexp] MRS subset_trans));
 
 (** Induction **)
 
@@ -70,22 +70,22 @@
 by (rtac notI 1);
 by (etac (In1_inject RS (In0_not_In1 RS notE)) 1);
 qed "CONST_not_COMB";
-val COMB_not_CONST = standard (CONST_not_COMB RS not_sym);
-val CONST_neq_COMB = standard (CONST_not_COMB RS notE);
+bind_thm ("COMB_not_CONST", (CONST_not_COMB RS not_sym));
+bind_thm ("CONST_neq_COMB", (CONST_not_COMB RS notE));
 val COMB_neq_CONST = sym RS CONST_neq_COMB;
 
 goalw UTerm.thy uterm_con_defs "~ COMB(u,v) = VAR(x)";
 by (rtac In1_not_In0 1);
 qed "COMB_not_VAR";
-val VAR_not_COMB = standard (COMB_not_VAR RS not_sym);
-val COMB_neq_VAR = standard (COMB_not_VAR RS notE);
+bind_thm ("VAR_not_COMB", (COMB_not_VAR RS not_sym));
+bind_thm ("COMB_neq_VAR", (COMB_not_VAR RS notE));
 val VAR_neq_COMB = sym RS COMB_neq_VAR;
 
 goalw UTerm.thy uterm_con_defs "~ VAR(x) = CONST(c)";
 by (rtac In0_not_In1 1);
 qed "VAR_not_CONST";
-val CONST_not_VAR = standard (VAR_not_CONST RS not_sym);
-val VAR_neq_CONST = standard (VAR_not_CONST RS notE);
+bind_thm ("CONST_not_VAR", (VAR_not_CONST RS not_sym));
+bind_thm ("VAR_neq_CONST", (VAR_not_CONST RS notE));
 val CONST_neq_VAR = sym RS VAR_neq_CONST;
 
 
@@ -93,24 +93,24 @@
 by (rtac (CONST_not_COMB RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
 by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
 qed "Const_not_Comb";
-val Comb_not_Const = standard (Const_not_Comb RS not_sym);
-val Const_neq_Comb = standard (Const_not_Comb RS notE);
+bind_thm ("Comb_not_Const", (Const_not_Comb RS not_sym));
+bind_thm ("Const_neq_Comb", (Const_not_Comb RS notE));
 val Comb_neq_Const = sym RS Const_neq_Comb;
 
 goalw UTerm.thy [Comb_def,Var_def] "~ Comb(u,v) = Var(x)";
 by (rtac (COMB_not_VAR RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
 by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
 qed "Comb_not_Var";
-val Var_not_Comb = standard (Comb_not_Var RS not_sym);
-val Comb_neq_Var = standard (Comb_not_Var RS notE);
+bind_thm ("Var_not_Comb", (Comb_not_Var RS not_sym));
+bind_thm ("Comb_neq_Var", (Comb_not_Var RS notE));
 val Var_neq_Comb = sym RS Comb_neq_Var;
 
 goalw UTerm.thy [Var_def,Const_def] "~ Var(x) = Const(c)";
 by (rtac (VAR_not_CONST RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
 by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
 qed "Var_not_Const";
-val Const_not_Var = standard (Var_not_Const RS not_sym);
-val Var_neq_Const = standard (Var_not_Const RS notE);
+bind_thm ("Const_not_Var", (Var_not_Const RS not_sym));
+bind_thm ("Var_neq_Const", (Var_not_Const RS notE));
 val Const_neq_Var = sym RS Var_neq_Const;
 
 
@@ -131,9 +131,9 @@
 by (fast_tac inject_cs 1);
 qed "COMB_COMB_eq";
 
-val VAR_inject = standard (VAR_VAR_eq RS iffD1);
-val CONST_inject = standard (CONST_CONST_eq RS iffD1);
-val COMB_inject = standard (COMB_COMB_eq RS iffD1 RS conjE);
+bind_thm ("VAR_inject", (VAR_VAR_eq RS iffD1));
+bind_thm ("CONST_inject", (CONST_CONST_eq RS iffD1));
+bind_thm ("COMB_inject", (COMB_COMB_eq RS iffD1 RS conjE));
 
 
 (*For reasoning about abstract uterm constructors*)
@@ -148,17 +148,17 @@
 goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)";
 by (fast_tac uterm_cs 1);
 qed "Var_Var_eq";
-val Var_inject = standard (Var_Var_eq RS iffD1);
+bind_thm ("Var_inject", (Var_Var_eq RS iffD1));
 
 goalw UTerm.thy [Const_def] "(Const(x)=Const(y)) = (x=y)";
 by (fast_tac uterm_cs 1);
 qed "Const_Const_eq";
-val Const_inject = standard (Const_Const_eq RS iffD1);
+bind_thm ("Const_inject", (Const_Const_eq RS iffD1));
 
 goalw UTerm.thy [Comb_def] "(Comb(u,v)=Comb(x,y)) = (u=x & v=y)";
 by (fast_tac uterm_cs 1);
 qed "Comb_Comb_eq";
-val Comb_inject = standard (Comb_Comb_eq RS iffD1 RS conjE);
+bind_thm ("Comb_inject", (Comb_Comb_eq RS iffD1 RS conjE));
 
 val [major] = goal UTerm.thy "VAR(M): uterm(A) ==> M : A";
 by (rtac (major RS setup_induction) 1);
diff -r 4d0545e93c0d -r c533bc92e882 Sum.ML
--- a/Sum.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/Sum.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -40,7 +40,7 @@
 by (rtac Inr_RepI 1);
 qed "Inl_not_Inr";
 
-val Inl_neq_Inr = standard (Inl_not_Inr RS notE);
+bind_thm ("Inl_neq_Inr", (Inl_not_Inr RS notE));
 val Inr_neq_Inl = sym RS Inl_neq_Inr;
 
 goal Sum.thy "(Inl(a)=Inr(b)) = False";
diff -r 4d0545e93c0d -r c533bc92e882 Univ.ML
--- a/Univ.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/Univ.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -131,9 +131,9 @@
 			  Pair_inject, sym RS Push_neq_K0] 1
      ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1));
 qed "Scons_not_Atom";
-val Atom_not_Scons = standard (Scons_not_Atom RS not_sym);
+bind_thm ("Atom_not_Scons", (Scons_not_Atom RS not_sym));
 
-val Scons_neq_Atom = standard (Scons_not_Atom RS notE);
+bind_thm ("Scons_neq_Atom", (Scons_not_Atom RS notE));
 val Atom_neq_Scons = sym RS Scons_neq_Atom;
 
 (*** Injectiveness ***)
@@ -224,9 +224,9 @@
 goalw Univ.thy [Leaf_def,o_def] "(M$N) ~= Leaf(a)";
 by (rtac Scons_not_Atom 1);
 qed "Scons_not_Leaf";
-val Leaf_not_Scons = standard (Scons_not_Leaf RS not_sym);
+bind_thm ("Leaf_not_Scons", (Scons_not_Leaf RS not_sym));
 
-val Scons_neq_Leaf = standard (Scons_not_Leaf RS notE);
+bind_thm ("Scons_neq_Leaf", (Scons_not_Leaf RS notE));
 val Leaf_neq_Scons = sym RS Scons_neq_Leaf;
 
 (** Scons vs Numb **)
@@ -234,9 +234,9 @@
 goalw Univ.thy [Numb_def,o_def] "(M$N) ~= Numb(k)";
 by (rtac Scons_not_Atom 1);
 qed "Scons_not_Numb";
-val Numb_not_Scons = standard (Scons_not_Numb RS not_sym);
+bind_thm ("Numb_not_Scons", (Scons_not_Numb RS not_sym));
 
-val Scons_neq_Numb = standard (Scons_not_Numb RS notE);
+bind_thm ("Scons_neq_Numb", (Scons_not_Numb RS notE));
 val Numb_neq_Scons = sym RS Scons_neq_Numb;
 
 (** Leaf vs Numb **)
@@ -244,9 +244,9 @@
 goalw Univ.thy [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)";
 by (simp_tac (HOL_ss addsimps [Atom_Atom_eq,Inl_not_Inr]) 1);
 qed "Leaf_not_Numb";
-val Numb_not_Leaf = standard (Leaf_not_Numb RS not_sym);
+bind_thm ("Numb_not_Leaf", (Leaf_not_Numb RS not_sym));
 
-val Leaf_neq_Numb = standard (Leaf_not_Numb RS notE);
+bind_thm ("Leaf_neq_Numb", (Leaf_not_Numb RS notE));
 val Numb_neq_Leaf = sym RS Leaf_neq_Numb;
 
 
@@ -392,8 +392,8 @@
 by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
 qed "In0_not_In1";
 
-val In1_not_In0 = standard (In0_not_In1 RS not_sym);
-val In0_neq_In1 = standard (In0_not_In1 RS notE);
+bind_thm ("In1_not_In0", (In0_not_In1 RS not_sym));
+bind_thm ("In0_neq_In1", (In0_not_In1 RS notE));
 val In1_neq_In0 = sym RS In0_neq_In1;
 
 val [major] = goalw Univ.thy [In0_def] "In0(M) = In0(N) ==>  M=N";
diff -r 4d0545e93c0d -r c533bc92e882 WF.ML
--- a/WF.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/WF.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -111,7 +111,7 @@
 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
 by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
 qed "is_recfun_equal_lemma";
-val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
+bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp));
 
 
 val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]
diff -r 4d0545e93c0d -r c533bc92e882 ex/LList.ML
--- a/ex/LList.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/ex/LList.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -321,7 +321,7 @@
 qed "Lconst_fun_mono";
 
 (* Lconst(M) = CONS(M,Lconst(M)) *)
-val Lconst = standard (Lconst_fun_mono RS (Lconst_def RS def_lfp_Tarski));
+bind_thm ("Lconst", (Lconst_fun_mono RS (Lconst_def RS def_lfp_Tarski)));
 
 (*A typical use of co-induction to show membership in the gfp.
   The containing set is simply the singleton {Lconst(M)}. *)
@@ -365,9 +365,9 @@
 by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
 qed "LCons_not_LNil";
 
-val LNil_not_LCons = standard (LCons_not_LNil RS not_sym);
+bind_thm ("LNil_not_LCons", (LCons_not_LNil RS not_sym));
 
-val LCons_neq_LNil = standard (LCons_not_LNil RS notE);
+bind_thm ("LCons_neq_LNil", (LCons_not_LNil RS notE));
 val LNil_neq_LCons = sym RS LCons_neq_LNil;
 
 (** llist constructors **)
@@ -389,7 +389,7 @@
 by (fast_tac (HOL_cs addSEs [Scons_inject, make_elim In1_inject]) 1);
 qed "CONS_CONS_eq";
 
-val CONS_inject = standard (CONS_CONS_eq RS iffD1 RS conjE);
+bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
 
 
 (*For reasoning about abstract llist constructors*)
@@ -401,7 +401,7 @@
 goalw LList.thy [LCons_def] "(LCons(x,xs)=LCons(y,ys)) = (x=y & xs=ys)";
 by (fast_tac llist_cs 1);
 qed "LCons_LCons_eq";
-val LCons_inject = standard (LCons_LCons_eq RS iffD1 RS conjE);
+bind_thm ("LCons_inject", (LCons_LCons_eq RS iffD1 RS conjE));
 
 val [major] = goal LList.thy "CONS(M,N): llist(A) ==> M: A & N: llist(A)";
 by (rtac (major RS llist.elim) 1);
@@ -537,7 +537,7 @@
 by (ALLGOALS
     (asm_simp_tac Lappend_ss THEN'
      fast_tac (set_cs addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
-val Lappend_type = result();
+qed "Lappend_type";
 
 (*strong co-induction: bisimulation and case analysis on one variable*)
 goal LList.thy
@@ -863,7 +863,7 @@
 by (rtac (refl RS Pair_cong) 1);
 by (stac lmap_LNil 1);
 by (rtac refl 1);
-val lmap_lappend_distrib = result();
+qed "lmap_lappend_distrib";
 
 (*Shorter proof of theorem above using llist_equalityI as strong coinduction*)
 goal LList.thy "lmap(f, lappend(l,n)) = lappend(lmap(f,l), lmap(f,n))";
diff -r 4d0545e93c0d -r c533bc92e882 ex/PropLog.ML
--- a/ex/PropLog.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/ex/PropLog.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -26,7 +26,7 @@
 (* "[| G<=H;  G |- p |] ==> H |- p"
    This order of premises is convenient with RS
 *)
-val weaken_left = standard (thms_mono RS subsetD);
+bind_thm ("weaken_left", (thms_mono RS subsetD));
 
 (* H |- p ==> insert(a,H) |- p *)
 val weaken_left_insert = subset_insertI RS weaken_left;
@@ -58,7 +58,7 @@
 val thms_falseE = weaken_right RS (thms.DN RS thms.MP);
 
 (* [| H |- p->false;  H |- p;  q: pl |] ==> H |- q *)
-val thms_notE = standard (thms.MP RS thms_falseE);
+bind_thm ("thms_notE", (thms.MP RS thms_falseE));
 
 (** The function eval **)
 
diff -r 4d0545e93c0d -r c533bc92e882 ex/SList.ML
--- a/ex/SList.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/ex/SList.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -30,7 +30,7 @@
 qed "list_sexp";
 
 (* A <= sexp ==> list(A) <= sexp *)
-val list_subset_sexp = standard ([list_mono, list_sexp] MRS subset_trans);
+bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans));
 
 (*Induction for the type 'a list *)
 val prems = goalw SList.thy [Nil_def,Cons_def]
@@ -64,9 +64,9 @@
 goalw SList.thy list_con_defs "CONS(M,N) ~= NIL";
 by (rtac In1_not_In0 1);
 qed "CONS_not_NIL";
-val NIL_not_CONS = standard (CONS_not_NIL RS not_sym);
+bind_thm ("NIL_not_CONS", (CONS_not_NIL RS not_sym));
 
-val CONS_neq_NIL = standard (CONS_not_NIL RS notE);
+bind_thm ("CONS_neq_NIL", (CONS_not_NIL RS notE));
 val NIL_neq_CONS = sym RS CONS_neq_NIL;
 
 goalw SList.thy [Nil_def,Cons_def] "x # xs ~= Nil";
@@ -74,9 +74,9 @@
 by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
 qed "Cons_not_Nil";
 
-val Nil_not_Cons = standard (Cons_not_Nil RS not_sym);
+bind_thm ("Nil_not_Cons", (Cons_not_Nil RS not_sym));
 
-val Cons_neq_Nil = standard (Cons_not_Nil RS notE);
+bind_thm ("Cons_neq_Nil", (Cons_not_Nil RS notE));
 val Nil_neq_Cons = sym RS Cons_neq_Nil;
 
 (** Injectiveness of CONS and Cons **)
@@ -85,7 +85,7 @@
 by (fast_tac (HOL_cs addSEs [Scons_inject, make_elim In1_inject]) 1);
 qed "CONS_CONS_eq";
 
-val CONS_inject = standard (CONS_CONS_eq RS iffD1 RS conjE);
+bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
 
 (*For reasoning about abstract list constructors*)
 val list_cs = set_cs addIs [Rep_list] @ list.intrs
@@ -96,7 +96,7 @@
 goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
 by (fast_tac list_cs 1);
 qed "Cons_Cons_eq";
-val Cons_inject = standard (Cons_Cons_eq RS iffD1 RS conjE);
+bind_thm ("Cons_inject", (Cons_Cons_eq RS iffD1 RS conjE));
 
 val [major] = goal SList.thy "CONS(M,N): list(A) ==> M: A & N: list(A)";
 by (rtac (major RS setup_induction) 1);
diff -r 4d0545e93c0d -r c533bc92e882 ex/Simult.ML
--- a/ex/Simult.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/ex/Simult.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -155,37 +155,37 @@
 goalw Simult.thy TF_Rep_defs "(TCONS(K,M)=TCONS(L,N)) = (K=L & M=N)";
 by (fast_tac TF_Rep_cs 1);
 qed "TCONS_TCONS_eq";
-val TCONS_inject = standard (TCONS_TCONS_eq RS iffD1 RS conjE);
+bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
 
 goalw Simult.thy TF_Rep_defs "(FCONS(K,M)=FCONS(L,N)) = (K=L & M=N)";
 by (fast_tac TF_Rep_cs 1);
 qed "FCONS_FCONS_eq";
-val FCONS_inject = standard (FCONS_FCONS_eq RS iffD1 RS conjE);
+bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
 
 (** Distinctness of TCONS, FNIL and FCONS **)
 
 goalw Simult.thy TF_Rep_defs "TCONS(M,N) ~= FNIL";
 by (fast_tac TF_Rep_cs 1);
 qed "TCONS_not_FNIL";
-val FNIL_not_TCONS = standard (TCONS_not_FNIL RS not_sym);
+bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
 
-val TCONS_neq_FNIL = standard (TCONS_not_FNIL RS notE);
+bind_thm ("TCONS_neq_FNIL", (TCONS_not_FNIL RS notE));
 val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
 
 goalw Simult.thy TF_Rep_defs "FCONS(M,N) ~= FNIL";
 by (fast_tac TF_Rep_cs 1);
 qed "FCONS_not_FNIL";
-val FNIL_not_FCONS = standard (FCONS_not_FNIL RS not_sym);
+bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
 
-val FCONS_neq_FNIL = standard (FCONS_not_FNIL RS notE);
+bind_thm ("FCONS_neq_FNIL", (FCONS_not_FNIL RS notE));
 val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
 
 goalw Simult.thy TF_Rep_defs "TCONS(M,N) ~= FCONS(K,L)";
 by (fast_tac TF_Rep_cs 1);
 qed "TCONS_not_FCONS";
-val FCONS_not_TCONS = standard (TCONS_not_FCONS RS not_sym);
+bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
 
-val TCONS_neq_FCONS = standard (TCONS_not_FCONS RS notE);
+bind_thm ("TCONS_neq_FCONS", (TCONS_not_FCONS RS notE));
 val FCONS_neq_TCONS = sym RS TCONS_neq_FCONS;
 
 (*???? Too many derived rules ????
@@ -207,13 +207,13 @@
 goalw Simult.thy [Tcons_def] "(Tcons(x,xs)=Tcons(y,ys)) = (x=y & xs=ys)";
 by (fast_tac TF_cs 1);
 qed "Tcons_Tcons_eq";
-val Tcons_inject = standard (Tcons_Tcons_eq RS iffD1 RS conjE);
+bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
 
 goalw Simult.thy [Fcons_def,Fnil_def] "Fcons(x,xs) ~= Fnil";
 by (fast_tac TF_cs 1);
 qed "Fcons_not_Fnil";
 
-val Fcons_neq_Fnil = standard (Fcons_not_Fnil RS notE);;
+bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
 val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil;
 
 
@@ -222,7 +222,7 @@
 goalw Simult.thy [Fcons_def] "(Fcons(x,xs)=Fcons(y,ys)) = (x=y & xs=ys)";
 by (fast_tac TF_cs 1);
 qed "Fcons_Fcons_eq";
-val Fcons_inject = standard (Fcons_Fcons_eq RS iffD1 RS conjE);
+bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
 
 
 (*** TF_rec -- by wf recursion on pred_sexp ***)
diff -r 4d0545e93c0d -r c533bc92e882 ex/Term.ML
--- a/ex/Term.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/ex/Term.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -29,7 +29,7 @@
 qed "term_sexp";
 
 (* A <= sexp ==> term(A) <= sexp *)
-val term_subset_sexp = standard ([term_mono, term_sexp] MRS subset_trans);
+bind_thm ("term_subset_sexp", ([term_mono, term_sexp] MRS subset_trans));
 
 
 (** Elimination -- structural induction on the set term(A) **)