# HG changeset patch
# User wenzelm
# Date 1365447719 -7200
# Node ID d022e8bd2375387f60ac94d023e5f27479055bc2
# Parent  b7f908c99546dd5a7a8a5531cd59bb330a16e57c
improved printing of exception CTERM (see also d0f0f37ec346);

diff -r b7f908c99546 -r d022e8bd2375 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)