added Theory.nodes_of convenience;
authorwenzelm
Wed Apr 20 13:54:07 2011 +0200 (2011-04-20)
changeset 424252aa907d5ee4f
parent 42424 e94350a2ed20
child 42426 7ec150fcf3dc
added Theory.nodes_of convenience;
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/codegen.ML
src/Pure/theory.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Apr 20 13:17:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Apr 20 13:54:07 2011 +0200
     1.3 @@ -1272,7 +1272,7 @@
     1.4            |> maps snd |> map_filter #def
     1.5            |> Ord_List.make fast_string_ord
     1.6    in
     1.7 -    thy :: Theory.ancestors_of thy
     1.8 +    Theory.nodes_of thy
     1.9      |> maps Thm.axioms_of
    1.10      |> map (apsnd (subst_atomic subst o prop_of))
    1.11      |> sort (fast_string_ord o pairself fst)
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Apr 20 13:17:25 2011 +0200
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Apr 20 13:54:07 2011 +0200
     2.3 @@ -387,8 +387,7 @@
     2.4      val thy = Toplevel.theory_of state;
     2.5      val thy_session = Present.session_name thy;
     2.6  
     2.7 -    val all_thys = rev (thy :: Theory.ancestors_of thy);
     2.8 -    val gr = all_thys |> map (fn node =>
     2.9 +    val gr = rev (Theory.nodes_of thy) |> map (fn node =>
    2.10        let
    2.11          val name = Context.theory_name node;
    2.12          val parents = map Context.theory_name (Theory.parents_of node);
     3.1 --- a/src/Pure/codegen.ML	Wed Apr 20 13:17:25 2011 +0200
     3.2 +++ b/src/Pure/codegen.ML	Wed Apr 20 13:54:07 2011 +0200
     3.3 @@ -489,9 +489,11 @@
     3.4  
     3.5  fun mk_deftab thy =
     3.6    let
     3.7 -    val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
     3.8 -      (thy :: Theory.ancestors_of thy);
     3.9 -    fun add_def thyname (name, t) = (case dest_prim_def t of
    3.10 +    val axmss =
    3.11 +      map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
    3.12 +        (Theory.nodes_of thy);
    3.13 +    fun add_def thyname (name, t) =
    3.14 +      (case dest_prim_def t of
    3.15          NONE => I
    3.16        | SOME (s, (T, _)) => Symtab.map_default (s, [])
    3.17            (cons (T, (thyname, Thm.axiom thy name))));
     4.1 --- a/src/Pure/theory.ML	Wed Apr 20 13:17:25 2011 +0200
     4.2 +++ b/src/Pure/theory.ML	Wed Apr 20 13:54:07 2011 +0200
     4.3 @@ -11,6 +11,7 @@
     4.4    val assert_super: theory -> theory -> theory
     4.5    val parents_of: theory -> theory list
     4.6    val ancestors_of: theory -> theory list
     4.7 +  val nodes_of: theory -> theory list
     4.8    val check_thy: theory -> theory_ref
     4.9    val deref: theory_ref -> theory
    4.10    val merge: theory * theory -> theory
    4.11 @@ -52,6 +53,7 @@
    4.12  
    4.13  val parents_of = Context.parents_of;
    4.14  val ancestors_of = Context.ancestors_of;
    4.15 +fun nodes_of thy = thy :: ancestors_of thy;
    4.16  
    4.17  val check_thy = Context.check_thy;
    4.18  val deref = Context.deref;
    4.19 @@ -66,7 +68,7 @@
    4.20  val copy = Context.copy_thy;
    4.21  
    4.22  fun requires thy name what =
    4.23 -  if exists (fn thy' => Context.theory_name thy' = name) (thy :: ancestors_of thy) then ()
    4.24 +  if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then ()
    4.25    else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
    4.26  
    4.27  
    4.28 @@ -123,7 +125,7 @@
    4.29  val axiom_table = #2 o #axioms o rep_theory;
    4.30  
    4.31  val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
    4.32 -fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
    4.33 +fun all_axioms_of thy = maps axioms_of (nodes_of thy);
    4.34  
    4.35  val defs_of = #defs o rep_theory;
    4.36  
     5.1 --- a/src/Pure/thm.ML	Wed Apr 20 13:17:25 2011 +0200
     5.2 +++ b/src/Pure/thm.ML	Wed Apr 20 13:54:07 2011 +0200
     5.3 @@ -611,7 +611,7 @@
     5.4                 maxidx = maxidx, shyps = shyps, hyps = [], tpairs = [], prop = prop})
     5.5             end);
     5.6    in
     5.7 -    (case get_first get_ax (theory :: Theory.ancestors_of theory) of
     5.8 +    (case get_first get_ax (Theory.nodes_of theory) of
     5.9        SOME thm => thm
    5.10      | NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
    5.11    end;