drop_judgment: be graceful about undeclared judgment;
authorwenzelm
Wed Dec 12 18:05:44 2001 +0100 (2001-12-12)
changeset 12479ed46612ad7ec
parent 12478 ff7e534367b5
child 12480 32e67277a4b9
drop_judgment: be graceful about undeclared judgment;
src/Pure/Isar/object_logic.ML
     1.1 --- a/src/Pure/Isar/object_logic.ML	Wed Dec 12 18:03:10 2001 +0100
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Wed Dec 12 18:05:44 2001 +0100
     1.3 @@ -89,7 +89,8 @@
     1.4    | is_judgment _ _ = false;
     1.5  
     1.6  fun drop_judgment sg (Abs (x, T, t)) = Abs (x, T, drop_judgment sg t)
     1.7 -  | drop_judgment sg (tm as (Const (c, _) $ t)) = if c = judgment_name sg then t else tm
     1.8 +  | drop_judgment sg (tm as (Const (c, _) $ t)) =
     1.9 +      if (c = judgment_name sg handle TERM _ => false) then t else tm
    1.10    | drop_judgment _ tm = tm;
    1.11  
    1.12  fun fixed_judgment sg x =