# HG changeset patch
# User wenzelm
# Date 1546706000 -3600
# Node ID 81caae4fc4fa43fae3a28853bd95395c4d6cab41
# Parent  ff784d5a5bfb28b3346f6855a358f3c734af9fbe
eliminated spurious \<^print>;

diff -r ff784d5a5bfb -r 81caae4fc4fa src/HOL/Library/datatype_records.ML
--- a/src/HOL/Library/datatype_records.ML	Sat Jan 05 17:24:33 2019 +0100
+++ b/src/HOL/Library/datatype_records.ML	Sat Jan 05 17:33:20 2019 +0100
@@ -278,7 +278,7 @@
           NONE => raise Fail ("not a valid record field: " ^ name)
         | SOME s => Const (s, dummyT) $ Abs (Name.uu_, dummyT, arg)
       end
-  | field_update_tr _ t = raise TERM ("field_update_tr", [\<^print> t]);
+  | field_update_tr _ t = raise TERM ("field_update_tr", [t]);
 
 fun field_updates_tr ctxt (Const (\<^syntax_const>\<open>_datatype_field_updates\<close>, _) $ t $ u) =
       field_update_tr ctxt t :: field_updates_tr ctxt u