# HG changeset patch
# User haftmann
# Date 1261649158 -3600
# Node ID 248e1fd702e955061c35b3a3aca210eecef07872
# Parent  6ab14241ae0449721dadc569311e8337fcd1161e
made sml/nj happy

diff -r 6ab14241ae04 -r 248e1fd702e9 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Dec 23 17:37:42 2009 +0100
+++ b/src/Pure/Isar/code.ML	Thu Dec 24 11:05:58 2009 +0100
@@ -235,7 +235,7 @@
 
 type data = Object.T Datatab.table;
 fun create_data data = Synchronized.var "code data" data;
-fun empty_data () = create_data Datatab.empty;
+fun empty_data () = create_data Datatab.empty : data Synchronized.var;
 
 structure Code_Data = TheoryDataFun
 (