# HG changeset patch
# User wenzelm
# Date 1008176744 -3600
# Node ID ed46612ad7ecec8b435b12bd8a9f30d782f71df7
# Parent  ff7e534367b5d8ee7937a4571703d02b8764477f
drop_judgment: be graceful about undeclared judgment;

diff -r ff7e534367b5 -r ed46612ad7ec src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Dec 12 18:03:10 2001 +0100
+++ b/src/Pure/Isar/object_logic.ML	Wed Dec 12 18:05:44 2001 +0100
@@ -89,7 +89,8 @@
   | is_judgment _ _ = false;
 
 fun drop_judgment sg (Abs (x, T, t)) = Abs (x, T, drop_judgment sg t)
-  | drop_judgment sg (tm as (Const (c, _) $ t)) = if c = judgment_name sg then t else tm
+  | drop_judgment sg (tm as (Const (c, _) $ t)) =
+      if (c = judgment_name sg handle TERM _ => false) then t else tm
   | drop_judgment _ tm = tm;
 
 fun fixed_judgment sg x =