# HG changeset patch
# User nipkow
# Date 794669726 -3600
# Node ID 8477483f663f8d4ab600ede2c27dde58a08e4e12
# Parent  d9edeb96b51ccb4fb7997a00adadbfdfc8784aeb
Replaced read by read_cterm.

diff -r d9edeb96b51c -r 8477483f663f src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Mar 08 14:01:08 1995 +0100
+++ b/src/Provers/splitter.ML	Wed Mar 08 14:35:26 1995 +0100
@@ -19,10 +19,13 @@
 fun mk_case_split_tac iffD =
 let
 
-val lift = prove_goalw_cterm [] (cterm_of (sign_of (theory_of_thm iffD))
-             (read "[| !!x::'b::logic. Q(x) == R(x) |] ==> \
-                   \P(%x.Q(x)) == P(%x.R(x))::'a::logic"))
-             (fn [prem] => [rewtac prem, rtac reflexive_thm 1]);
+val lift =
+  let val ct = read_cterm (#sign(rep_thm iffD))
+           ("[| !!x::'b::logic. Q(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])
+  end;
 
 val trlift = lift RS transitive_thm;
 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;