# HG changeset patch
# User berghofe
# Date 879863450 -3600
# Node ID fc85fd71842987c370fe3a300a5622205e6c278d
# Parent  c4f1d3940d9599175425277942c75f75d2c9828e
Fixed bug in inst_split.

diff -r c4f1d3940d95 -r fc85fd718429 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Mon Nov 17 15:40:25 1997 +0100
+++ b/src/Provers/splitter.ML	Tue Nov 18 15:30:50 1997 +0100
@@ -234,7 +234,7 @@
       val sg = #sign(rep_thm state)
       val tsig = #tsig(Sign.rep_sg sg)
       val cntxt = mk_cntxt_splitthm t tt TB;
-      val T = fastype_of cntxt;
+      val T = fastype_of1 (Ts, cntxt);
       val ixnTs = Type.typ_match tsig ([],(PT2, T))
       val abss = foldl (fn (t, T) => Abs ("", T, t))
   in