added assert_judgment;
authorwenzelm
Wed Jul 10 14:49:06 2002 +0200 (2002-07-10)
changeset 1333427149d72bdff
parent 13333 1f5745b76fb8
child 13335 7995b3f4ca5e
added assert_judgment;
src/Pure/Isar/object_logic.ML
     1.1 --- a/src/Pure/Isar/object_logic.ML	Wed Jul 10 14:48:08 2002 +0200
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Wed Jul 10 14:49:06 2002 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4    val judgment_name: Sign.sg -> string
     1.5    val is_judgment: Sign.sg -> term -> bool
     1.6    val drop_judgment: Sign.sg -> term -> term
     1.7 +  val assert_judgment: Sign.sg -> term -> term
     1.8    val fixed_judgment: Sign.sg -> string -> term
     1.9    val declare_atomize: theory attribute
    1.10    val declare_rulify: theory attribute
    1.11 @@ -95,6 +96,11 @@
    1.12        if (c = judgment_name sg handle TERM _ => false) then t else tm
    1.13    | drop_judgment _ tm = tm;
    1.14  
    1.15 +fun assert_judgment sg (Abs (x, T, t)) = Abs (x, T, assert_judgment sg t)
    1.16 +  | assert_judgment sg t =
    1.17 +      if (is_judgment sg t handle TERM _ => true) then t
    1.18 +      else Const (judgment_name sg, fastype_of t --> propT) $ t;
    1.19 +
    1.20  fun fixed_judgment sg x =
    1.21    let  (*be robust wrt. low-level errors*)
    1.22      val c = judgment_name sg;