# HG changeset patch
# User wenzelm
# Date 1392673160 -3600
# Node ID 384bfd19ee615e99181aaa2153d2f0ec8a38f1e7
# Parent  76979adf0b96c8fdf21f493f21eac9dcea825efc
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);

diff -r 76979adf0b96 -r 384bfd19ee61 NEWS
--- a/NEWS	Mon Feb 17 21:37:41 2014 +0100
+++ b/NEWS	Mon Feb 17 22:39:20 2014 +0100
@@ -358,6 +358,13 @@
 pass runtime Proof.context (and ensure that the simplified entity
 actually belongs to it).
 
+* Subtle change of semantics of Thm.eq_thm: theory stamps are not
+compared (according to Thm.thm_ord), but assumed to be covered by the
+current background theory.  Thus equivalent data produced in different
+branches of the theory graph usually coincides (e.g. relevant for
+theory merge).  Note that the softer Thm.eq_thm_prop is often more
+appropriate than Thm.eq_thm.
+
 
 *** System ***
 
diff -r 76979adf0b96 -r 384bfd19ee61 src/Doc/IsarImplementation/Tactic.thy
--- a/src/Doc/IsarImplementation/Tactic.thy	Mon Feb 17 21:37:41 2014 +0100
+++ b/src/Doc/IsarImplementation/Tactic.thy	Mon Feb 17 22:39:20 2014 +0100
@@ -920,9 +920,8 @@
   "thm"} has fewer than @{text "n"} premises.
 
   \item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text
-  "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.  Both theorems must have
-  compatible background theories.  Both theorems must have the same
-  conclusions, the same set of hypotheses, and the same set of sort
+  "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.  Both theorems must have the
+  same conclusions, the same set of hypotheses, and the same set of sort
   hypotheses.  Names of bound variables are ignored as usual.
 
   \item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether
diff -r 76979adf0b96 -r 384bfd19ee61 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Feb 17 21:37:41 2014 +0100
+++ b/src/Pure/context.ML	Mon Feb 17 22:39:20 2014 +0100
@@ -43,7 +43,6 @@
   val this_theory: theory -> string -> theory
   val eq_thy: theory * theory -> bool
   val subthy: theory * theory -> bool
-  val joinable: theory * theory -> bool
   val merge: theory * theory -> theory
   val finish_thy: theory -> theory
   val begin_thy: (theory -> pretty) -> string -> theory list -> theory
@@ -246,8 +245,6 @@
 
 fun subthy thys = eq_thy thys orelse proper_subthy thys;
 
-fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
-
 
 (* consistent ancestors *)
 
diff -r 76979adf0b96 -r 384bfd19ee61 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Feb 17 21:37:41 2014 +0100
+++ b/src/Pure/more_thm.ML	Mon Feb 17 22:39:20 2014 +0100
@@ -37,7 +37,6 @@
   val thm_cache: (thm -> 'a) -> thm -> 'a
   val is_reflexive: thm -> bool
   val eq_thm: thm * thm -> bool
-  val eq_thm_thy: thm * thm -> bool
   val eq_thm_prop: thm * thm -> bool
   val eq_thm_strict: thm * thm -> bool
   val equiv_thm: thm * thm -> bool
@@ -191,17 +190,17 @@
 fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th))
   handle TERM _ => false;
 
-fun eq_thm ths =
-  Context.joinable (pairself Thm.theory_of_thm ths) andalso
-  is_equal (thm_ord ths);
+val eq_thm = is_equal o thm_ord;
 
-val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
 val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
 
 fun eq_thm_strict ths =
-  eq_thm_thy ths andalso eq_thm ths andalso
-    let val (rep1, rep2) = pairself Thm.rep_thm ths
-    in #maxidx rep1 = #maxidx rep2 andalso #tags rep1 = #tags rep2 end;
+  eq_thm ths andalso
+    let val (rep1, rep2) = pairself Thm.rep_thm ths in
+      Theory.eq_thy (#thy rep1, #thy rep2) andalso
+      #maxidx rep1 = #maxidx rep2 andalso
+      #tags rep1 = #tags rep2
+    end;
 
 
 (* pattern equivalence *)