Replaced read by read_cterm.
authornipkow
Wed Mar 08 14:35:26 1995 +0100 (1995-03-08)
changeset 9438477483f663f
parent 942 d9edeb96b51c
child 944 01d6571fa106
Replaced read by read_cterm.
src/Provers/splitter.ML
     1.1 --- a/src/Provers/splitter.ML	Wed Mar 08 14:01:08 1995 +0100
     1.2 +++ b/src/Provers/splitter.ML	Wed Mar 08 14:35:26 1995 +0100
     1.3 @@ -19,10 +19,13 @@
     1.4  fun mk_case_split_tac iffD =
     1.5  let
     1.6  
     1.7 -val lift = prove_goalw_cterm [] (cterm_of (sign_of (theory_of_thm iffD))
     1.8 -             (read "[| !!x::'b::logic. Q(x) == R(x) |] ==> \
     1.9 -                   \P(%x.Q(x)) == P(%x.R(x))::'a::logic"))
    1.10 -             (fn [prem] => [rewtac prem, rtac reflexive_thm 1]);
    1.11 +val lift =
    1.12 +  let val ct = read_cterm (#sign(rep_thm iffD))
    1.13 +           ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
    1.14 +            \P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT)
    1.15 +  in prove_goalw_cterm [] ct
    1.16 +     (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
    1.17 +  end;
    1.18  
    1.19  val trlift = lift RS transitive_thm;
    1.20  val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;