changeset 10411 | c7375583fe4e |
parent 10403 | 2955ee2424ce |
child 10652 | e6a4bb832b46 |
--- 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])