# HG changeset patch
# User wenzelm
# Date 960316303 -7200
# Node ID 20ff649a0fd1858801d08985da156723ef0079cc
# Parent  63d20536971f2a9b916784c2e6f41a7295acbe4d
added rule_params;

diff -r 63d20536971f -r 20ff649a0fd1 src/Provers/split_paired_all.ML
--- a/src/Provers/split_paired_all.ML	Tue Jun 06 20:31:22 2000 +0200
+++ b/src/Provers/split_paired_all.ML	Tue Jun 06 20:31:43 2000 +0200
@@ -12,6 +12,7 @@
 
 signature SPLIT_PAIRED_ALL =
 sig
+  val rule_params: string -> string -> thm -> thm
   val rule: thm -> thm
 end;
 
@@ -25,7 +26,7 @@
 val op ==> = Logic.mk_implies;
 
 
-fun rule raw_surj_pair =
+fun rule_params a b raw_surj_pair =
   let
     val ct = Thm.cterm_of (Thm.sign_of_thm raw_surj_pair);
 
@@ -37,7 +38,7 @@
     val P = Free (variant used "P", pT --> propT);
 
    (*"!!a b. PROP (a, b)"*)
-   val all_a_b = all "a" aT (all "b" bT (P $ (con $ Bound 1 $ Bound 0)));
+   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);
 
@@ -57,5 +58,7 @@
      (fn prems => [resolve_tac prems 1]);
   in standard (Thm.equal_intr lem4 lem3) end;
 
+val rule = rule_params "a" "b";
+
 
 end;