# HG changeset patch
# User wenzelm
# Date 908961038 -7200
# Node ID 1ddf7e1e8b193ec885aa01ac9427254975731157
# Parent  53b00681c63b86f57f1534b93abd00018696f9f3
improved var names;
tuned;

diff -r 53b00681c63b -r 1ddf7e1e8b19 src/Provers/split_paired_all.ML
--- a/src/Provers/split_paired_all.ML	Tue Oct 20 18:04:23 1998 +0200
+++ b/src/Provers/split_paired_all.ML	Wed Oct 21 11:10:38 1998 +0200
@@ -29,37 +29,31 @@
   let
     val ct = Thm.cterm_of (Thm.sign_of_thm raw_surj_pair);
 
-    val surj_pair = Drule.unvarify raw_surj_pair;
+    val surj_pair = Drule.unvarify (standard raw_surj_pair);
     val used = Term.add_term_names (#prop (Thm.rep_thm surj_pair), []);
 
     val (p, con $ _ $ _) = Logic.dest_equals (#prop (rep_thm surj_pair));
     val pT as Type (_, [aT, bT]) = fastype_of p;
-
     val P = Free (variant used "P", pT --> propT);
-    val x_name = variant used "x";
-    val x = Free (x_name, pT);
-    val a = variant used "a";
-    val b = variant used "b";
 
-   (*"P x == P (fst x, snd x)"*)
-   val lem1 =
-     Thm.combination (Thm.reflexive (ct P)) surj_pair
-     |> Thm.forall_intr (ct p)
-     |> Thm.forall_elim (ct x);
+   (*"!!a b. PROP (a, b)"*)
+   val all_a_b = all "a" aT (all "b" bT (P $ (con $ Bound 1 $ Bound 0)));
+   (*"!!x. PROP P x"*)
+   val all_x = all "x" pT (P $ Bound 0);
 
-   (*"!!a b. PROP (a, b) ==> PROP P x"*)
-   val lem2 = prove_goalw_cterm [lem1]
-     (ct (all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0))) ==> P $ x))
+   (*lemma "P p == P (fst p, snd p)"*)
+   val lem1 = Thm.combination (Thm.reflexive (ct P)) surj_pair;
+
+   (*lemma "!!a b. PROP (a, b) ==> PROP P p"*)
+   val lem2 = prove_goalw_cterm [lem1] (ct (all_a_b ==> P $ p))
      (fn prems => [resolve_tac prems 1]);
 
-   (*"!!a b. PROP (a, b) ==> !! x. PROP P x"*)
-   val lem3 = prove_goalw_cterm []
-     (ct (all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0))) ==> all x_name pT (P $ Bound 0)))
+   (*lemma "!!a b. PROP (a, b) ==> !!x. PROP P x"*)
+   val lem3 = prove_goalw_cterm [] (ct (all_a_b ==> all_x))
      (fn prems => [rtac lem2 1, resolve_tac prems 1]);
 
-   (*"!! x. PROP P x ==> !!a b. PROP (a, b)"*)
-   val lem4 = prove_goalw_cterm []
-     (ct (all x_name pT (P $ Bound 0) ==> all a aT (all a bT (P $ (con $ Bound 1 $ Bound 0)))))
+   (*lemma "!!x. PROP P x ==> !!a b. PROP (a, b)"*)
+   val lem4 = prove_goalw_cterm [] (ct (all_x ==> all_a_b))
      (fn prems => [resolve_tac prems 1]);
   in standard (Thm.equal_intr lem4 lem3) end;