# HG changeset patch
# User wenzelm
# Date 1026305346 -7200
# Node ID 27149d72bdff0609425884fef9cb9131432a6be2
# Parent  1f5745b76fb80774df9106e056396300397b81f5
added assert_judgment;

diff -r 1f5745b76fb8 -r 27149d72bdff src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Jul 10 14:48:08 2002 +0200
+++ b/src/Pure/Isar/object_logic.ML	Wed Jul 10 14:49:06 2002 +0200
@@ -13,6 +13,7 @@
   val judgment_name: Sign.sg -> string
   val is_judgment: Sign.sg -> term -> bool
   val drop_judgment: Sign.sg -> term -> term
+  val assert_judgment: Sign.sg -> term -> term
   val fixed_judgment: Sign.sg -> string -> term
   val declare_atomize: theory attribute
   val declare_rulify: theory attribute
@@ -95,6 +96,11 @@
       if (c = judgment_name sg handle TERM _ => false) then t else tm
   | drop_judgment _ tm = tm;
 
+fun assert_judgment sg (Abs (x, T, t)) = Abs (x, T, assert_judgment sg t)
+  | assert_judgment sg t =
+      if (is_judgment sg t handle TERM _ => true) then t
+      else Const (judgment_name sg, fastype_of t --> propT) $ t;
+
 fun fixed_judgment sg x =
   let  (*be robust wrt. low-level errors*)
     val c = judgment_name sg;