--- a/src/Provers/splitter.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Provers/splitter.ML Tue Jun 01 12:33:50 2004 +0200
@@ -76,8 +76,8 @@
val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
val lift =
let val ct = read_cterm (#sign(rep_thm Data.iffD))
- ("[| !!x. (Q::('b::logic)=>('c::logic))(x) == R(x) |] ==> \
- \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
+ ("[| !!x. (Q::('b::{})=>('c::{}))(x) == R(x) |] ==> \
+ \P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT)
in prove_goalw_cterm [] ct
(fn [prem] => [rewtac prem, rtac reflexive_thm 1])
end;