diff -r 3a8d722fd3ff -r 16c4ea954511 ex/LexProd.ML
--- a/ex/LexProd.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/ex/LexProd.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -12,7 +12,7 @@
 by (rtac allI 1);
 by (rtac (surjective_pairing RS ssubst) 1);
 by (fast_tac HOL_cs 1);
-val split_all_pair = result();
+qed "split_all_pair";
 
 val [wfa,wfb] = goalw LexProd.thy [wf_def,LexProd.lex_prod_def]
  "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
@@ -21,4 +21,4 @@
 by (EVERY1 [rtac allI,rtac impI]);
 by (rtac (wfb RS spec RS mp) 1);
 by (fast_tac (set_cs addSEs [Pair_inject]) 1);
-val wf_lex_prod = result();
+qed "wf_lex_prod";