# HG changeset patch
# User haftmann
# Date 1348381459 -7200
# Node ID e016736fbe0aedc4978b2f0048c7caf8136670b9
# Parent  791e6fc53f73b4491ba5fa7814c5781c2625af18
make smlnj happy

diff -r 791e6fc53f73 -r e016736fbe0a src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Sep 22 21:59:40 2012 +0200
+++ b/src/Pure/Isar/code.ML	Sun Sep 23 08:24:19 2012 +0200
@@ -293,7 +293,7 @@
 
 (* access to executable code *)
 
-val the_exec = fst o Code_Data.get;
+val the_exec : theory -> spec = fst o Code_Data.get;
 
 fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));