# HG changeset patch
# User haftmann
# Date 1348506695 -7200
# Node ID 47e4178f9a94bc3d3d8acc42fbc0c06e765293f6
# Parent  fb2128470345af01f91f5e575198c8fe850d2f10
made smlnj even happier

diff -r fb2128470345 -r 47e4178f9a94 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Sep 24 17:52:44 2012 +0200
+++ b/src/Pure/Isar/code.ML	Mon Sep 24 19:11:35 2012 +0200
@@ -283,7 +283,7 @@
   type T = spec * (data * theory_ref) option Synchronized.var;
   val empty = (make_spec (false, (Symtab.empty,
     (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
-  val extend = apsnd (K (empty_dataref ()));
+  val extend : T -> T = apsnd (K (empty_dataref ()));
   fun merge ((spec1, _), (spec2, _)) =
     (merge_spec (spec1, spec2), empty_dataref ());
 );