# HG changeset patch
# User wenzelm
# Date 1131442992 -3600
# Node ID 77b6d06ad99d9433f1c58fe92bad3da92f8ccfaa
# Parent  41328805d4dbd826613d15992e2549f637d51428
renamed assert_prop to ensure_prop;

diff -r 41328805d4db -r 77b6d06ad99d src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Tue Nov 08 10:43:11 2005 +0100
+++ b/src/Pure/Isar/object_logic.ML	Tue Nov 08 10:43:12 2005 +0100
@@ -13,7 +13,7 @@
   val is_judgment: theory -> term -> bool
   val drop_judgment: theory -> term -> term
   val fixed_judgment: theory -> string -> term
-  val assert_propT: theory -> term -> term
+  val ensure_propT: theory -> term -> term
   val declare_atomize: theory attribute
   val declare_rulify: theory attribute
   val atomize_term: theory -> term -> term
@@ -110,7 +110,7 @@
     val U = Term.domain_type T handle Match => aT;
   in Const (c, T) $ Free (x, U) end;
 
-fun assert_propT thy t =
+fun ensure_propT thy t =
   let val T = Term.fastype_of t
   in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;