src/Provers/splitter.ML
changeset 3835 9a5a4e123859
parent 3537 79ac9b475621
child 3918 94e0fdcb7b91
     1.1 --- a/src/Provers/splitter.ML	Fri Oct 10 15:51:38 1997 +0200
     1.2 +++ b/src/Provers/splitter.ML	Fri Oct 10 15:52:12 1997 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  val lift =
     1.5    let val ct = read_cterm (#sign(rep_thm iffD))
     1.6             ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
     1.7 -            \P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT)
     1.8 +            \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
     1.9    in prove_goalw_cterm [] ct
    1.10       (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
    1.11    end;