# HG changeset patch
# User wenzelm
# Date 1439741970 -7200
# Node ID b710a5087116ca7edb9e97672d2000bb4fc7ea36
# Parent  d5f7b424ba479ce4006efd339bcacf49d577c82d
prefer theory_id operations;
tuned signature;

diff -r d5f7b424ba47 -r b710a5087116 src/Doc/Implementation/Prelim.thy
--- a/src/Doc/Implementation/Prelim.thy	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Sun Aug 16 18:19:30 2015 +0200
@@ -121,8 +121,8 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type theory} \\
-  @{index_ML Theory.eq_thy: "theory * theory -> bool"} \\
-  @{index_ML Theory.subthy: "theory * theory -> bool"} \\
+  @{index_ML Context.eq_thy: "theory * theory -> bool"} \\
+  @{index_ML Context.subthy: "theory * theory -> bool"} \\
   @{index_ML Theory.merge: "theory * theory -> theory"} \\
   @{index_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\
   @{index_ML Theory.parents_of: "theory -> theory list"} \\
@@ -133,10 +133,10 @@
 
   \item Type @{ML_type theory} represents theory contexts.
 
-  \item @{ML "Theory.eq_thy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} check strict
+  \item @{ML "Context.eq_thy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} check strict
   identity of two theories.
 
-  \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} compares theories
+  \item @{ML "Context.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} compares theories
   according to the intrinsic graph structure of the construction.
   This sub-theory relation is a nominal approximation of inclusion
   (@{text "\<subseteq>"}) of the corresponding content (according to the
diff -r d5f7b424ba47 -r b710a5087116 src/HOL/Matrix_LP/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -607,7 +607,7 @@
     val thy = theory_of computer
     val _ = check_compatible computer th
     val _ =
-      Theory.subthy (theory_of_theorem th, thy) orelse raise Compute "modus_ponens: bad theory"
+      Context.subthy (theory_of_theorem th, thy) orelse raise Compute "modus_ponens: bad theory"
     val th' = make_theorem computer (Thm.transfer thy raw_th') []
     val varsubst = varsubst_of_theorem th
     fun run vars_allowed t =
diff -r d5f7b424ba47 -r b710a5087116 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -809,7 +809,7 @@
       end;
 
     fun maybe_restore lthy_old lthy =
-      lthy |> not (Theory.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy)))
+      lthy |> not (Context.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy)))
         ? Local_Theory.restore;
 
     val map_bind_def =
diff -r d5f7b424ba47 -r b710a5087116 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -220,7 +220,7 @@
 (* FIXME: reintroduce code before new release:
 
     val nitpick_thy = Thy_Info.get_theory "Nitpick"
-    val _ = Theory.subthy (nitpick_thy, thy) orelse
+    val _ = Context.subthy (nitpick_thy, thy) orelse
             error "You must import the theory \"Nitpick\" to use Nitpick"
 *)
     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
diff -r d5f7b424ba47 -r b710a5087116 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -1358,13 +1358,14 @@
 (* Ideally we would check against "Complex_Main", not "Hilbert_Choice", but any
    theory will do as long as it contains all the "axioms" and "axiomatization"
    commands. *)
-fun is_built_in_theory thy = Theory.subthy (thy, @{theory Hilbert_Choice})
+fun is_built_in_theory thy_id =
+  Context.subthy_id (thy_id, Context.theory_id @{theory Hilbert_Choice})
 
 fun all_nondefs_of ctxt subst =
   ctxt |> Spec_Rules.get
        |> filter (curry (op =) Spec_Rules.Unknown o fst)
        |> maps (snd o snd)
-       |> filter_out (is_built_in_theory o Thm.theory_of_thm)
+       |> filter_out (is_built_in_theory o Thm.theory_id_of_thm)
        |> map (subst_atomic subst o Thm.prop_of)
 
 fun arity_of_built_in_const (s, T) =
diff -r d5f7b424ba47 -r b710a5087116 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -351,7 +351,7 @@
   | normalize_eq t = t
 
 fun if_thm_before th th' =
-  if Theory.subthy (apply2 Thm.theory_of_thm (th, th')) then th else th'
+  if Context.subthy_id (apply2 Thm.theory_id_of_thm (th, th')) then th else th'
 
 (* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level
    facts, so that MaSh can learn from the low-level proofs. *)
diff -r d5f7b424ba47 -r b710a5087116 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -768,30 +768,39 @@
 fun class_feature_of s = "s" ^ s
 val local_feature = "local"
 
-fun crude_theory_ord p =
-  if Theory.subthy p then
-    if Theory.eq_thy p then EQUAL else LESS
-  else if Theory.subthy (swap p) then
-    GREATER
-  else
-    (case int_ord (apply2 (length o Theory.ancestors_of) p) of
-      EQUAL => string_ord (apply2 Context.theory_name p)
-    | order => order)
+fun crude_thm_ord ctxt =
+  let
+    val ancestor_lengths =
+      fold (fn thy => Symtab.update (Context.theory_name thy, length (Context.ancestors_of thy)))
+        (Theory.nodes_of (Proof_Context.theory_of ctxt)) Symtab.empty
+    val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name
+    fun crude_theory_ord p =
+      if Context.eq_thy_id p then EQUAL
+      else if Context.proper_subthy_id p then LESS
+      else if Context.proper_subthy_id (swap p) then GREATER
+      else
+        (case apply2 ancestor_length p of
+          (SOME m, SOME n) =>
+            (case int_ord (m, n) of
+              EQUAL => string_ord (apply2 Context.theory_id_name p)
+            | ord => ord)
+        | _ => string_ord (apply2 Context.theory_id_name p))
+  in
+    fn p =>
+      (case crude_theory_ord (apply2 Thm.theory_id_of_thm p) of
+        EQUAL =>
+        (* The hack below is necessary because of odd dependencies that are not reflected in the theory
+           comparison. *)
+        let val q = apply2 (nickname_of_thm ctxt) p in
+          (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
+          (case bool_ord (apply2 (String.isSuffix "_def") (swap q)) of
+            EQUAL => string_ord q
+          | ord => ord)
+        end
+      | ord => ord)
+  end;
 
-fun crude_thm_ord ctxt p =
-  (case crude_theory_ord (apply2 Thm.theory_of_thm p) of
-    EQUAL =>
-    (* The hack below is necessary because of odd dependencies that are not reflected in the theory
-       comparison. *)
-    let val q = apply2 (nickname_of_thm ctxt) p in
-      (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
-      (case bool_ord (apply2 (String.isSuffix "_def") (swap q)) of
-        EQUAL => string_ord q
-      | ord => ord)
-    end
-  | ord => ord)
-
-val thm_less_eq = Theory.subthy o apply2 Thm.theory_of_thm
+val thm_less_eq = Context.subthy_id o apply2 Thm.theory_id_of_thm
 fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p))
 
 val freezeT = Type.legacy_freeze_type
@@ -1110,12 +1119,11 @@
     find_maxes Symtab.empty ([], Graph.maximals G)
   end
 
-fun strict_subthy thyp = Theory.subthy thyp andalso not (Theory.subthy (swap thyp))
-
 fun maximal_wrt_access_graph _ _ [] = []
   | maximal_wrt_access_graph ctxt access_G ((fact as (_, th)) :: facts) =
-    let val thy = Thm.theory_of_thm th in
-      fact :: filter_out (fn (_, th') => strict_subthy (Thm.theory_of_thm th', thy)) facts
+    let val thy_id = Thm.theory_id_of_thm th in
+      fact :: filter_out (fn (_, th') =>
+        Context.proper_subthy_id (Thm.theory_id_of_thm th', thy_id)) facts
       |> map (nickname_of_thm ctxt o snd)
       |> maximal_wrt_graph access_G
     end
diff -r d5f7b424ba47 -r b710a5087116 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/Isar/code.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -339,7 +339,7 @@
     val dataref = (snd o Code_Data.get) theory;
     val (datatab, thy) = case Synchronized.value dataref
      of SOME (datatab, thy) =>
-        if Theory.eq_thy (theory, thy)
+        if Context.eq_thy (theory, thy)
           then (datatab, thy)
           else (Datatab.empty, theory)
       | NONE => (Datatab.empty, theory)
diff -r d5f7b424ba47 -r b710a5087116 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -491,7 +491,7 @@
     val thy = Proof_Context.theory_of ctxt;
 
     val _ =
-      Theory.subthy (Thm.theory_of_thm goal, thy) orelse
+      Context.subthy_id (Thm.theory_id_of_thm goal, Context.theory_id thy) orelse
         error "Bad background theory of goal state";
     val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
 
diff -r d5f7b424ba47 -r b710a5087116 src/Pure/Tools/thy_deps.ML
--- a/src/Pure/Tools/thy_deps.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/Tools/thy_deps.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -22,7 +22,7 @@
   | gen_thy_deps prep_thy ctxt bounds =
       let
         val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
-        val rel = Theory.subthy o swap;
+        val rel = Context.subthy o swap;
         val pred =
           (case upper of
             SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
@@ -38,7 +38,7 @@
 val thy_deps =
   gen_thy_deps (fn ctxt => fn thy =>
     let val thy0 = Proof_Context.theory_of ctxt
-    in if Theory.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
+    in if Context.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
 
 val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Theory.check;
 
diff -r d5f7b424ba47 -r b710a5087116 src/Pure/context.ML
--- a/src/Pure/context.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/context.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -34,7 +34,7 @@
   type pretty
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
-  val theory_name_id: theory_id -> string
+  val theory_id_name: theory_id -> string
   val theory_name: theory -> string
   val PureN: string
   val display_names: theory -> string list
@@ -196,7 +196,7 @@
 fun make_history name stage = {name = name, stage = stage};
 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
 
-val theory_name_id = #name o history_of_id;
+val theory_id_name = #name o history_of_id;
 val theory_name = #name o history_of;
 val parents_of = #parents o ancestry_of;
 val ancestors_of = #ancestors o ancestry_of;
diff -r d5f7b424ba47 -r b710a5087116 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/goal.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -209,7 +209,7 @@
       | SOME st =>
           let
             val _ =
-              Theory.subthy (Thm.theory_of_thm st, thy) orelse
+              Context.subthy_id (Thm.theory_id_of_thm st, Context.theory_id thy) orelse
                 err "Bad background theory of goal state";
             val res =
               (finish ctxt' st
diff -r d5f7b424ba47 -r b710a5087116 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/more_thm.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -195,7 +195,7 @@
 fun eq_thm_strict ths =
   eq_thm ths andalso
     let val (rep1, rep2) = apply2 Thm.rep_thm ths in
-      Theory.eq_thy (#thy rep1, #thy rep2) andalso
+      Context.eq_thy (#thy rep1, #thy rep2) andalso
       #maxidx rep1 = #maxidx rep2 andalso
       #tags rep1 = #tags rep2
     end;
diff -r d5f7b424ba47 -r b710a5087116 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/theory.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -6,8 +6,6 @@
 
 signature THEORY =
 sig
-  val eq_thy: theory * theory -> bool
-  val subthy: theory * theory -> bool
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val nodes_of: theory -> theory list
@@ -40,9 +38,6 @@
 
 (** theory context operations **)
 
-val eq_thy = Context.eq_thy;
-val subthy = Context.subthy;
-
 val parents_of = Context.parents_of;
 val ancestors_of = Context.ancestors_of;
 fun nodes_of thy = thy :: ancestors_of thy;
diff -r d5f7b424ba47 -r b710a5087116 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/thm.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -71,6 +71,7 @@
   val terms_of_tpairs: (term * term) list -> term list
   val full_prop_of: thm -> term
   val theory_of_thm: thm -> theory
+  val theory_id_of_thm: thm -> Context.theory_id
   val theory_name_of_thm: thm -> string
   val maxidx_of: thm -> int
   val maxidx_thm: thm -> int -> int
@@ -206,10 +207,10 @@
   let
     val Cterm {thy, t, T, maxidx, sorts} = ct;
     val _ =
-      Theory.subthy (thy, thy') orelse
+      Context.subthy (thy, thy') orelse
         raise CTERM ("transfer_cterm: not a super theory", [ct]);
   in
-    if Theory.eq_thy (thy, thy') then ct
+    if Context.eq_thy (thy, thy') then ct
     else Cterm {thy = thy', t = t, T = T, maxidx = maxidx, sorts = sorts}
   end;
 
@@ -400,7 +401,9 @@
 (* basic components *)
 
 val theory_of_thm = #thy o rep_thm;
-val theory_name_of_thm = Context.theory_name o #thy o rep_thm;
+val theory_id_of_thm = Context.theory_id o #thy o rep_thm;
+val theory_name_of_thm = Context.theory_id_name o theory_id_of_thm;
+
 val maxidx_of = #maxidx o rep_thm;
 fun maxidx_thm th i = Int.max (maxidx_of th, i);
 val hyps_of = #hyps o rep_thm;
@@ -429,9 +432,9 @@
 fun transfer thy' thm =
   let
     val Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop}) = thm;
-    val _ = Theory.subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]);
+    val _ = Context.subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]);
   in
-    if Theory.eq_thy (thy, thy') then thm
+    if Context.eq_thy (thy, thy') then thm
     else
       Thm (der,
        {thy = thy',
@@ -452,7 +455,7 @@
 
 fun make_context NONE thy = Context.Theory thy
   | make_context (SOME ctxt) thy =
-      if Theory.subthy (thy, Proof_Context.theory_of ctxt) then Context.Proof ctxt
+      if Context.subthy (thy, Proof_Context.theory_of ctxt) then Context.Proof ctxt
       else raise THEORY ("Bad context", [thy, Proof_Context.theory_of ctxt]);
 
 (*explicit weakening: maps |- B to A |- B*)
@@ -572,7 +575,7 @@
     fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
     val Thm (Deriv {promises, ...}, {thy, shyps, hyps, tpairs, prop, ...}) = thm;
 
-    val _ = Theory.eq_thy (thy, orig_thy) orelse err "bad theory";
+    val _ = Context.eq_thy (thy, orig_thy) orelse err "bad theory";
     val _ = prop aconv orig_prop orelse err "bad prop";
     val _ = null tpairs orelse err "bad tpairs";
     val _ = null hyps orelse err "bad hyps";