improved printing of exception CTERM (see also d0f0f37ec346);
authorwenzelm
Mon, 08 Apr 2013 21:01:59 +0200
changeset 51640 d022e8bd2375
parent 51639 b7f908c99546
child 51641 cd05e9fcc63d
child 51653 97de25c51b2d
improved printing of exception CTERM (see also d0f0f37ec346);
src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Mon Apr 08 17:10:49 2013 +0200
+++ b/src/Pure/Isar/runtime.ML	Mon Apr 08 21:01:59 2013 +0200
@@ -103,6 +103,9 @@
                     if_context context Syntax.string_of_term ts))
             | TERM (msg, ts) =>
                 raised exn "TERM" (msg :: if_context context Syntax.string_of_term ts)
+            | CTERM (msg, cts) =>
+                raised exn "CTERM"
+                  (msg :: if_context context Syntax.string_of_term (map term_of cts))
             | THM (msg, i, thms) =>
                 raised exn ("THM " ^ string_of_int i)
                   (msg :: if_context context Display.string_of_thm thms)