src/Provers/splitter.ML
changeset 20237 5daab2c78b8e
parent 20217 25b068a99d2b
child 20664 ffbc5a57191a
--- 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)) =