--- a/src/HOL/Tools/record.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/HOL/Tools/record.ML Wed Dec 01 15:03:44 2010 +0100
@@ -1869,7 +1869,7 @@
(fn _ => fn eq_def => tac eq_def) eq_def)
|-> (fn eq_def => fn thy => thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
|> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
- |> ensure_random_record ext_tyco vs (fst ext) ((fst o strip_type o snd) ext)
+ |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
end;