src/Provers/splitter.ML

--- a/src/Provers/splitter.ML	Fri Oct 21 18:14:37 2005 +0200
+++ b/src/Provers/splitter.ML	Fri Oct 21 18:14:38 2005 +0200
@@ -73,7 +73,7 @@
   let val ct = read_cterm (#sign(rep_thm Data.iffD))
            ("[| !!x. (Q::('b::{})=>('c::{}))(x) == R(x) |] ==> \
             \P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT)
-  in prove_goalw_cterm [] ct
+  in OldGoals.prove_goalw_cterm [] ct
      (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
   end;