--- 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"
--- 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)
--- 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 *)