# HG changeset patch
# User wenzelm
# Date 1183560574 -7200
# Node ID b65692d4adcd9bfed2cc456485f30bd956f2518c
# Parent  c00b12a4e245859112c7fe4c337f89bb6ac664b5
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;

diff -r c00b12a4e245 -r b65692d4adcd src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Jul 04 14:21:00 2007 +0200
+++ b/src/HOL/HOL.thy	Wed Jul 04 16:49:34 2007 +0200
@@ -1674,7 +1674,8 @@
 
 method_setup normalization = {*
   Method.no_args (Method.SIMPLE_METHOD'
-    (CONVERSION (HOLogic.Trueprop_conv NBE.normalization_conv) THEN' resolve_tac [TrueI, refl]))
+    (CONVERSION (ObjectLogic.judgment_conv NBE.normalization_conv)
+      THEN' resolve_tac [TrueI, refl]))
 *} "solve goal by normalization"
 
 
diff -r c00b12a4e245 -r b65692d4adcd src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Wed Jul 04 14:21:00 2007 +0200
+++ b/src/HOL/hologic.ML	Wed Jul 04 16:49:34 2007 +0200
@@ -19,7 +19,6 @@
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
   val dest_cTrueprop: cterm -> cterm
-  val Trueprop_conv: conv -> conv
   val conj_intr: thm -> thm -> thm
   val conj_elim: thm -> thm * thm
   val conj_elims: thm -> thm list
@@ -145,10 +144,6 @@
   if can dest_Trueprop (Thm.term_of ct) then Thm.dest_arg ct
   else raise CTERM ("cdest_Trueprop", [ct]);
 
-fun Trueprop_conv conv ct =
-  if can dest_Trueprop (Thm.term_of ct) then Conv.arg_conv conv ct
-  else raise CTERM ("Trueprop_conv", [ct]);
-
 fun conj_intr thP thQ =
   let
     val (P, Q) = pairself (dest_cTrueprop o Thm.cprop_of) (thP, thQ)
diff -r c00b12a4e245 -r b65692d4adcd src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Jul 04 14:21:00 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML	Wed Jul 04 16:49:34 2007 +0200
@@ -14,6 +14,7 @@
   val drop_judgment: theory -> term -> term
   val fixed_judgment: theory -> string -> term
   val ensure_propT: theory -> term -> term
+  val judgment_conv: conv -> conv
   val is_elim: thm -> bool
   val declare_atomize: attribute
   val declare_rulify: attribute
@@ -80,7 +81,7 @@
 end;
 
 
-(* term operations *)
+(* judgments *)
 
 fun judgment_name thy =
   (case ObjectLogicData.get thy of
@@ -109,6 +110,11 @@
   let val T = Term.fastype_of t
   in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
 
+fun judgment_conv cv ct =
+  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
+  then Conv.arg_conv cv ct
+  else raise CTERM ("judgment_conv", [ct]);
+
 
 (* elimination rules *)