# HG changeset patch
# User wenzelm
# Date 1374046328 -7200
# Node ID 77146b576ac7ecdebd5d2b72a8b14743d9008a95
# Parent  c16f35e5a5aa3861a5f94dc1230d8859363de879
tuned;

diff -r c16f35e5a5aa -r 77146b576ac7 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Jul 16 23:34:33 2013 +0200
+++ b/src/Pure/context.ML	Wed Jul 17 09:32:08 2013 +0200
@@ -495,7 +495,7 @@
 fun raw_transfer thy' (Proof.Context (data, thy_ref)) =
   let
     val thy = deref thy_ref;
-    val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";
+    val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory";
     val _ = check_thy thy;
     val data' = init_new_data data thy';
     val thy_ref' = check_thy thy';
@@ -518,9 +518,9 @@
   in k end;
 
 fun get k dest prf =
-  dest (case Datatab.lookup (data_of_proof prf) k of
+  (case Datatab.lookup (data_of_proof prf) k of
     SOME x => x
-  | NONE => invoke_init k (Proof_Context.theory_of prf));   (*adhoc value*)
+  | NONE => invoke_init k (Proof_Context.theory_of prf)) |> dest;  (*adhoc value for old theories*)
 
 fun put k mk x = map_prf (Datatab.update (k, mk x));