src/HOL/Tools/record.ML

--- a/src/HOL/Tools/record.ML	Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/Tools/record.ML	Fri Oct 12 15:08:29 2012 +0200
@@ -112,7 +112,7 @@
     val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
   in
     thy
-    |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
+    |> Typedef.add_typedef_global (SOME raw_tyco) (raw_tyco, vs, NoSyn)
         (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;