# HG changeset patch
# User wenzelm
# Date 979850496 -3600
# Node ID 2c85f2416c1ba5592f2612a5343414fca46eef83
# Parent  5651e0636e385078dda576161afbcbeeb92755b7
made SML/XL happy;

diff -r 5651e0636e38 -r 2c85f2416c1b src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Jan 18 20:40:47 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Jan 18 21:41:36 2001 +0100
@@ -619,7 +619,8 @@
 
 
 (*local goals*)
-fun local_goal' prepp kind check f name atts args int state =
+fun local_goal' prepp kind (check: bool -> state -> state)
+    f name atts args int state =
   state
   |> setup_goal open_block prepp kind f name atts args
   |> warn_extra_tfrees state