# HG changeset patch
# User wenzelm
# Date 1183586785 -7200
# Node ID 7d6b1d800dc42b52d8c1e49451108217ed85ae1e
# Parent  f07ef41ffb8721568ec7faf49e8b73b4abf85a34
avoid polymorphic equality;
added dest_judgment;

diff -r f07ef41ffb87 -r 7d6b1d800dc4 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Thu Jul 05 00:06:24 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML	Thu Jul 05 00:06:25 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 dest_judgment: cterm -> cterm
   val judgment_conv: conv -> conv
   val is_elim: thm -> bool
   val declare_atomize: attribute
@@ -46,7 +47,7 @@
   val extend = I;
 
   fun merge_judgment (SOME x, SOME y) =
-        if x = y then SOME x else error "Attempt to merge different object-logics"
+        if (x: string) = y then SOME x else error "Attempt to merge different object-logics"
     | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
 
   fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
@@ -110,6 +111,11 @@
   let val T = Term.fastype_of t
   in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
 
+fun dest_judgment ct =
+  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
+  then Thm.dest_arg ct
+  else raise CTERM ("dest_judgment", [ct]);
+
 fun judgment_conv cv ct =
   if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
   then Conv.arg_conv cv ct
@@ -148,7 +154,7 @@
 (* atomize *)
 
 fun rewrite_prems_tac rews =
-  CONVERSION (Conv.forall_conv ~1 (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true rews))));
+  CONVERSION (Conv.forall_conv ~1 (Conv.prems_conv ~1 (MetaSimplifier.rewrite true rews)));
 
 fun atomize_term thy =
   drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];