diff -r 12dd5d2e266b -r 978854c19b5e Prod.ML
--- a/Prod.ML	Thu Nov 24 20:31:09 1994 +0100
+++ b/Prod.ML	Fri Nov 25 09:12:16 1994 +0100
@@ -67,7 +67,7 @@
 qed "Pair_fst_snd_eq";
 
 (*Prevents simplification of c: much faster*)
-val split_weak_cong = prove_goal Prod.thy
+qed_goal "split_weak_cong" Prod.thy
   "p=q ==> split(c,p) = split(c,q)"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
@@ -152,12 +152,12 @@
 
 (*** Disjoint union of a family of sets - Sigma ***)
 
-val SigmaI = prove_goalw Prod.thy [Sigma_def]
+qed_goalw "SigmaI" Prod.thy [Sigma_def]
     "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
 
 (*The general elimination rule*)
-val SigmaE = prove_goalw Prod.thy [Sigma_def]
+qed_goalw "SigmaE" Prod.thy [Sigma_def]
     "[| c: Sigma(A,B);  \
 \       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \
 \    |] ==> P"
@@ -166,17 +166,17 @@
     (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
 
 (** Elimination of <a,b>:A*B -- introduces no eigenvariables **)
-val SigmaD1 = prove_goal Prod.thy "<a,b> : Sigma(A,B) ==> a : A"
+qed_goal "SigmaD1" Prod.thy "<a,b> : Sigma(A,B) ==> a : A"
  (fn [major]=>
   [ (rtac (major RS SigmaE) 1),
     (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
 
-val SigmaD2 = prove_goal Prod.thy "<a,b> : Sigma(A,B) ==> b : B(a)"
+qed_goal "SigmaD2" Prod.thy "<a,b> : Sigma(A,B) ==> b : B(a)"
  (fn [major]=>
   [ (rtac (major RS SigmaE) 1),
     (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
 
-val SigmaE2 = prove_goal Prod.thy
+qed_goal "SigmaE2" Prod.thy
     "[| <a,b> : Sigma(A,B);    \
 \       [| a:A;  b:B(a) |] ==> P   \
 \    |] ==> P"