--- 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 =