handle "Rep_unit" & Co. gracefully
authorblanchet
Thu, 05 Aug 2010 18:33:07 +0200
changeset 38208 10417cd47448
parent 38207 792b78e355e7
child 38209 3d1d928dce50
handle "Rep_unit" & Co. gracefully
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