# HG changeset patch
# User wenzelm
# Date 1303300447 -7200
# Node ID 2aa907d5ee4f2ae18cb0b4c77437b99e42f4ee69
# Parent  e94350a2ed20d34b79de8e6ced5272343838d777
added Theory.nodes_of convenience;

diff -r e94350a2ed20 -r 2aa907d5ee4f src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Apr 20 13:17:25 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Apr 20 13:54:07 2011 +0200
@@ -1272,7 +1272,7 @@
           |> maps snd |> map_filter #def
           |> Ord_List.make fast_string_ord
   in
-    thy :: Theory.ancestors_of thy
+    Theory.nodes_of thy
     |> maps Thm.axioms_of
     |> map (apsnd (subst_atomic subst o prop_of))
     |> sort (fast_string_ord o pairself fst)
diff -r e94350a2ed20 -r 2aa907d5ee4f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Apr 20 13:17:25 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Apr 20 13:54:07 2011 +0200
@@ -387,8 +387,7 @@
     val thy = Toplevel.theory_of state;
     val thy_session = Present.session_name thy;
 
-    val all_thys = rev (thy :: Theory.ancestors_of thy);
-    val gr = all_thys |> map (fn node =>
+    val gr = rev (Theory.nodes_of thy) |> map (fn node =>
       let
         val name = Context.theory_name node;
         val parents = map Context.theory_name (Theory.parents_of node);
diff -r e94350a2ed20 -r 2aa907d5ee4f src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Apr 20 13:17:25 2011 +0200
+++ b/src/Pure/codegen.ML	Wed Apr 20 13:54:07 2011 +0200
@@ -489,9 +489,11 @@
 
 fun mk_deftab thy =
   let
-    val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
-      (thy :: Theory.ancestors_of thy);
-    fun add_def thyname (name, t) = (case dest_prim_def t of
+    val axmss =
+      map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
+        (Theory.nodes_of thy);
+    fun add_def thyname (name, t) =
+      (case dest_prim_def t of
         NONE => I
       | SOME (s, (T, _)) => Symtab.map_default (s, [])
           (cons (T, (thyname, Thm.axiom thy name))));
diff -r e94350a2ed20 -r 2aa907d5ee4f src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Apr 20 13:17:25 2011 +0200
+++ b/src/Pure/theory.ML	Wed Apr 20 13:54:07 2011 +0200
@@ -11,6 +11,7 @@
   val assert_super: theory -> theory -> theory
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
+  val nodes_of: theory -> theory list
   val check_thy: theory -> theory_ref
   val deref: theory_ref -> theory
   val merge: theory * theory -> theory
@@ -52,6 +53,7 @@
 
 val parents_of = Context.parents_of;
 val ancestors_of = Context.ancestors_of;
+fun nodes_of thy = thy :: ancestors_of thy;
 
 val check_thy = Context.check_thy;
 val deref = Context.deref;
@@ -66,7 +68,7 @@
 val copy = Context.copy_thy;
 
 fun requires thy name what =
-  if exists (fn thy' => Context.theory_name thy' = name) (thy :: ancestors_of thy) then ()
+  if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then ()
   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
 
 
@@ -123,7 +125,7 @@
 val axiom_table = #2 o #axioms o rep_theory;
 
 val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
-fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
+fun all_axioms_of thy = maps axioms_of (nodes_of thy);
 
 val defs_of = #defs o rep_theory;
 
diff -r e94350a2ed20 -r 2aa907d5ee4f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Apr 20 13:17:25 2011 +0200
+++ b/src/Pure/thm.ML	Wed Apr 20 13:54:07 2011 +0200
@@ -611,7 +611,7 @@
                maxidx = maxidx, shyps = shyps, hyps = [], tpairs = [], prop = prop})
            end);
   in
-    (case get_first get_ax (theory :: Theory.ancestors_of theory) of
+    (case get_first get_ax (Theory.nodes_of theory) of
       SOME thm => thm
     | NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
   end;