# HG changeset patch
# User wenzelm
# Date 1208278159 -7200
# Node ID 2e363edf75780edf91fb2bd9934875dcb17dc514
# Parent  167d879a89b097bffebf500e2bd07b8514bd5f53
Theory.eq_thy;

diff -r 167d879a89b0 -r 2e363edf7578 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Apr 15 18:49:18 2008 +0200
+++ b/src/Pure/more_thm.ML	Tue Apr 15 18:49:19 2008 +0200
@@ -135,7 +135,7 @@
 
 val eq_thms = eq_list eq_thm;
 
-val eq_thm_thy = eq_thy o pairself Thm.theory_of_thm;
+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;
 
 
diff -r 167d879a89b0 -r 2e363edf7578 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Tue Apr 15 18:49:18 2008 +0200
+++ b/src/Pure/old_goals.ML	Tue Apr 15 18:49:19 2008 +0200
@@ -175,7 +175,7 @@
             val {hyps, prop, ...} = Thm.rep_thm th
             val final_th = standard th
         in  if not check then final_th
-            else if not (eq_thy(thy,thy')) then !result_error_fn state
+            else if not (Theory.eq_thy(thy,thy')) then !result_error_fn state
                 ("Theory of proof state has changed!" ^
                  thy_error (thy,thy'))
             else if ngoals>0 then !result_error_fn state
@@ -189,7 +189,7 @@
             else  !result_error_fn state "proved a different theorem"
         end
   in
-     if eq_thy(thy, Thm.theory_of_thm st0)
+     if Theory.eq_thy(thy, Thm.theory_of_thm st0)
      then (prems, st0, mkresult)
      else error ("Definitions would change the proof state's theory" ^
                  thy_error (thy, Thm.theory_of_thm st0))
diff -r 167d879a89b0 -r 2e363edf7578 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Apr 15 18:49:18 2008 +0200
+++ b/src/Pure/thm.ML	Tue Apr 15 18:49:19 2008 +0200
@@ -420,8 +420,8 @@
   let
     val Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop} = thm;
     val thy = Theory.deref thy_ref;
-    val _ = subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]);
-    val is_eq = eq_thy (thy, thy');
+    val _ = Theory.subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]);
+    val is_eq = Theory.eq_thy (thy, thy');
     val _ = Theory.check_thy thy;
   in
     if is_eq then thm