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";