src/Provers/splitter.ML
changeset 927 305e7cfda869
parent 231 cb6a24451544
child 943 8477483f663f
     1.1 --- a/src/Provers/splitter.ML	Fri Mar 03 12:34:57 1995 +0100
     1.2 +++ b/src/Provers/splitter.ML	Fri Mar 03 12:48:06 1995 +0100
     1.3 @@ -19,9 +19,10 @@
     1.4  fun mk_case_split_tac iffD =
     1.5  let
     1.6  
     1.7 -val lift = prove_goal Pure.thy
     1.8 -  "[| !!x::'b::logic. Q(x) == R(x) |] ==> P(%x.Q(x)) == P(%x.R(x))::'a::logic"
     1.9 -  (fn [prem] => [rewtac prem, rtac reflexive_thm 1]);
    1.10 +val lift = prove_goalw_cterm [] (cterm_of (sign_of (theory_of_thm iffD))
    1.11 +             (read "[| !!x::'b::logic. Q(x) == R(x) |] ==> \
    1.12 +                   \P(%x.Q(x)) == P(%x.R(x))::'a::logic"))
    1.13 +             (fn [prem] => [rewtac prem, rtac reflexive_thm 1]);
    1.14  
    1.15  val trlift = lift RS transitive_thm;
    1.16  val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;