# HG changeset patch
# User webertj
# Date 1154002917 -7200
# Node ID 5daab2c78b8ec4996eb651153610901ac9710b74
# Parent  54e15870444bca950b4068a405a79119732407bb
type annotation added to make SML/NJ happy

diff -r 54e15870444b -r 5daab2c78b8e src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Thu Jul 27 13:44:03 2006 +0200
+++ b/src/Provers/splitter.ML	Thu Jul 27 14:21:57 2006 +0200
@@ -256,7 +256,7 @@
 
 (* (string * (Term.typ * Term.term * Thm.thm * Term.typ * int) list) list -> Context.theory -> Term.typ list -> Term.term ->
   (Thm.thm * (Term.typ * Term.typ * int list) list * int list * Term.typ * Term.term) list *)
-fun split_posns cmap sg Ts t =
+fun split_posns (cmap : (string * (typ * term * thm * typ * int) list) list) sg Ts t =
   let
     val T' = fastype_of1 (Ts, t);
     fun posns Ts pos apsns (Abs (_, T, t)) =