src/HOL/Tools/record.ML

--- a/src/HOL/Tools/record.ML	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/Tools/record.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -111,7 +111,7 @@
     val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
   in
     thy
-    |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
+    |> Typedef.add_typedef_global false (raw_tyco, vs, NoSyn)
         (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;