# HG changeset patch
# User paulson
# Date 914860139 -3600
# Node ID bd37dc0f56d971dfbaf1eccace4e24cc9451c598
# Parent  01f67f5f8dd09ce99255d5ab1d40a940ae7ffd81
comments

diff -r 01f67f5f8dd0 -r bd37dc0f56d9 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Dec 28 16:48:22 1998 +0100
+++ b/src/Pure/sign.ML	Mon Dec 28 16:48:59 1998 +0100
@@ -281,8 +281,11 @@
   error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg);
 
 fun err_uninit sg kind =
-  error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg);
+  error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ 
+	 of_theory sg);
 
+(*Trying to access theory data using get / put operations from a different
+  instance of the TheoryDataFun result.  Typical cure: re-load all files*)
 fun err_access sg kind =
   error ("Unauthorized access to " ^ quote kind ^ " data" ^ of_theory sg);