diff -r 3305f573294e -r b47d41d9f4b5 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/HOL/Tools/record.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -914,7 +914,7 @@
 fun record_tr' ctxt t =
   let
     val thy = ProofContext.theory_of ctxt;
-    val extern = Consts.extern (ProofContext.consts_of ctxt);
+    val extern = Consts.extern ctxt (ProofContext.consts_of ctxt);
 
     fun strip_fields t =
       (case strip_comb t of
@@ -957,7 +957,7 @@
 
 fun dest_update ctxt c =
   (case try Lexicon.unmark_const c of
-    SOME d => try (unsuffix updateN) (Consts.extern (ProofContext.consts_of ctxt) d)
+    SOME d => try (unsuffix updateN) (Consts.extern ctxt (ProofContext.consts_of ctxt) d)
   | NONE => NONE);
 
 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =