src/HOL/Univ.ML

 Goal "inj_on Abs_Node Node";
 by (rtac inj_on_inverseI 1);
 by (etac Abs_Node_inverse 1);
 qed "inj_on_Abs_Node";
 
-val Abs_Node_inject = inj_on_Abs_Node RS inj_onD;
+bind_thm ("Abs_Node_inject", inj_on_Abs_Node RS inj_onD);
 
 
 (*** Introduction rules for Node ***)
 
 Goalw [Node_def] "(%k. Inr 0, a) : Node";

 (** Atomic nodes **)
 
 Goalw [Atom_def] "inj(Atom)";
 by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inject]) 1);
 qed "inj_Atom";
-val Atom_inject = inj_Atom RS injD;
+bind_thm ("Atom_inject", inj_Atom RS injD);
 
 Goal "(Atom(a)=Atom(b)) = (a=b)";
 by (blast_tac (claset() addSDs [Atom_inject]) 1);
 qed "Atom_Atom_eq";
 AddIffs [Atom_Atom_eq];

 Goalw [Numb_def,o_def] "inj(Numb)";
 by (rtac injI 1);
 by (etac (Atom_inject RS Inr_inject) 1);
 qed "inj_Numb";
 
-val Numb_inject = inj_Numb RS injD;
+bind_thm ("Numb_inject", inj_Numb RS injD);
 AddSDs [Numb_inject];
 
 (** Injectiveness of Push_Node **)
 
 val [major,minor] = Goalw [Push_Node_def]

 
 Goal "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)";
 by (Blast_tac 1);
 qed "dprod_Sigma";
 
-val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
+bind_thm ("dprod_subset_Sigma", [dprod_mono, dprod_Sigma] MRS subset_trans |> standard);
 
 (*Dependent version*)
 Goal "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))";
 by Safe_tac;
 by (stac Split 1);

 
 Goal "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)";
 by (Blast_tac 1);
 qed "dsum_Sigma";
 
-val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
+bind_thm ("dsum_subset_Sigma", [dsum_mono, dsum_Sigma] MRS subset_trans |> standard);
 
 
 (*** Domain ***)
 
 Goal "Domain (dprod r s) = uprod (Domain r) (Domain s)";