src/Provers/splitter.ML
changeset 4236 fc85fd718429
parent 4232 29f3875596ad
child 4453 bcb28bb925c1
     1.1 --- a/src/Provers/splitter.ML	Mon Nov 17 15:40:25 1997 +0100
     1.2 +++ b/src/Provers/splitter.ML	Tue Nov 18 15:30:50 1997 +0100
     1.3 @@ -234,7 +234,7 @@
     1.4        val sg = #sign(rep_thm state)
     1.5        val tsig = #tsig(Sign.rep_sg sg)
     1.6        val cntxt = mk_cntxt_splitthm t tt TB;
     1.7 -      val T = fastype_of cntxt;
     1.8 +      val T = fastype_of1 (Ts, cntxt);
     1.9        val ixnTs = Type.typ_match tsig ([],(PT2, T))
    1.10        val abss = foldl (fn (t, T) => Abs ("", T, t))
    1.11    in