src/HOL/Tools/record.ML

--- a/src/HOL/Tools/record.ML	Sun Nov 09 18:27:43 2014 +0100
+++ b/src/HOL/Tools/record.ML	Sun Nov 09 20:41:53 2014 +0100
@@ -112,7 +112,7 @@
   in
     thy
     |> Typedef.add_typedef_global false (raw_tyco, vs, NoSyn)
-        (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
+        (HOLogic.mk_UNIV repT) NONE (fn _ => rtac UNIV_witness 1)
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;