Univ.ML

 by (rtac singletonI 1);
 by (REPEAT (eresolve_tac [imageE, Abs_Node_inject RS apfstE, 
 			  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);
-
-val Scons_neq_Atom = standard (Scons_not_Atom RS notE);
+bind_thm ("Atom_not_Scons", (Scons_not_Atom RS not_sym));
+
+bind_thm ("Scons_neq_Atom", (Scons_not_Atom RS notE));
 val Atom_neq_Scons = sym RS Scons_neq_Atom;
 
 (*** Injectiveness ***)
 
 (** Atomic nodes **)

 (** Scons vs Leaf **)
 
 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);
-
-val Scons_neq_Leaf = standard (Scons_not_Leaf RS notE);
+bind_thm ("Leaf_not_Scons", (Scons_not_Leaf RS not_sym));
+
+bind_thm ("Scons_neq_Leaf", (Scons_not_Leaf RS notE));
 val Leaf_neq_Scons = sym RS Scons_neq_Leaf;
 
 (** Scons vs Numb **)
 
 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);
-
-val Scons_neq_Numb = standard (Scons_not_Numb RS notE);
+bind_thm ("Numb_not_Scons", (Scons_not_Numb RS not_sym));
+
+bind_thm ("Scons_neq_Numb", (Scons_not_Numb RS notE));
 val Numb_neq_Scons = sym RS Scons_neq_Numb;
 
 (** Leaf vs Numb **)
 
 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);
-
-val Leaf_neq_Numb = standard (Leaf_not_Numb RS notE);
+bind_thm ("Numb_not_Leaf", (Leaf_not_Numb RS not_sym));
+
+bind_thm ("Leaf_neq_Numb", (Leaf_not_Numb RS notE));
 val Numb_neq_Leaf = sym RS Leaf_neq_Numb;
 
 
 (*** ndepth -- the depth of a node ***)
 

 goalw Univ.thy [In0_def,In1_def] "In0(M) ~= In1(N)";
 by (rtac notI 1);
 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";
 by (rtac (major RS Scons_inject2) 1);
 qed "In0_inject";