eliminated spurious \<^print>;
authorwenzelm
Sat, 05 Jan 2019 17:33:20 +0100
changeset 69598 81caae4fc4fa
parent 69597 ff784d5a5bfb
child 69599 caa7e406056d
eliminated spurious \<^print>;
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