# HG changeset patch
# User blanchet
# Date 1281025987 -7200
# Node ID 10417cd47448c0940133dcd6d9e904e9daa57b33
# Parent  792b78e355e7a37a831d608f7f56910509717643
handle "Rep_unit" & Co. gracefully

diff -r 792b78e355e7 -r 10417cd47448 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 18:00:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 18:33:07 2010 +0200
@@ -1729,8 +1729,7 @@
                        ts)
                     end
                   else
-                    raise TERM ("Nitpick_HOL.unfold_defs_in_term.do_const",
-                                [Const x])
+                    (Const x, ts)
                 end
               else if is_equational_fun_but_no_plain_def hol_ctxt x orelse
                       is_choice_spec_fun hol_ctxt x then