# HG changeset patch
# User berghofe
# Date 973615289 -3600
# Node ID c7375583fe4e4605e506f6832b79b5bd93447b4b
# Parent  1f8716b9e13e072d71ebf86f23c6e17aea45e199
Added type constraint in theorem "lift".

diff -r 1f8716b9e13e -r c7375583fe4e src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Tue Nov 07 09:33:14 2000 +0100
+++ b/src/Provers/splitter.ML	Tue Nov 07 17:41:29 2000 +0100
@@ -75,7 +75,7 @@
 val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
 val lift =
   let val ct = read_cterm (#sign(rep_thm Data.iffD))
-           ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
+           ("[| !!x. (Q::('b::logic)=>('c::logic))(x) == R(x) |] ==> \
             \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
   in prove_goalw_cterm [] ct
      (fn [prem] => [rewtac prem, rtac reflexive_thm 1])