1.1 --- a/src/Pure/Isar/code.ML	Mon Sep 24 17:52:44 2012 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Sep 24 19:11:35 2012 +0200
     1.3 @@ -283,7 +283,7 @@
     1.4    type T = spec * (data * theory_ref) option Synchronized.var;
     1.5    val empty = (make_spec (false, (Symtab.empty,
     1.6      (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
     1.7 -  val extend = apsnd (K (empty_dataref ()));
     1.8 +  val extend : T -> T = apsnd (K (empty_dataref ()));
     1.9    fun merge ((spec1, _), (spec2, _)) =
    1.10      (merge_spec (spec1, spec2), empty_dataref ());
    1.11  );