# HG changeset patch
# User wenzelm
# Date 769357066 -7200
# Node ID 921f87897a765ad0532ff7870e353d4be8e3f1f1
# Parent  a8d204d8071d392250bba4a738554466d383c7c9
added print_sign, print_axioms: theory -> unit;
replaced ["logic"] by logicS;

diff -r a8d204d8071d -r 921f87897a76 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu May 19 16:16:36 1994 +0200
+++ b/src/Pure/drule.ML	Thu May 19 16:17:46 1994 +0200
@@ -41,6 +41,8 @@
   val print_ctyp: ctyp -> unit
   val print_goals: int -> thm -> unit
   val print_goals_ref: (int -> thm -> unit) ref
+  val print_sign: theory -> unit
+  val print_axioms: theory -> unit
   val print_theory: theory -> unit
   val print_thm: thm -> unit
   val prth: thm -> thm
@@ -182,20 +184,21 @@
 
 val pprint_theory = Sign.pprint_sg o sign_of;
 
-fun print_theory thy =
+val print_sign = Sign.print_sg o sign_of;
+
+fun print_axioms thy =
   let
-    fun prt_thm (name, thm) = Pretty.block
-      [Pretty.str (name ^ ":"), Pretty.brk 1, Pretty.quote (pretty_thm thm)];
+    val {sign, ext_axtab, ...} = rep_theory thy;
+    val axioms = Symtab.dest ext_axtab;
 
-    val sg = sign_of thy;
-    val axioms =        (* FIXME should rather fix axioms_of *)
-      sort (fn ((x, _), (y, _)) => x <= y)
-        (gen_distinct eq_fst (axioms_of thy));
+    fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
+      Pretty.quote (Sign.pretty_term sign t)];
   in
-    Sign.print_sg sg;
-    Pretty.writeln (Pretty.big_list "axioms:" (map prt_thm axioms))
+    Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms))
   end;
 
+fun print_theory thy = (print_sign thy; print_axioms thy);
+
 
 
 (** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **)
@@ -428,7 +431,7 @@
 
 
 val reflexive_thm =
-  let val cx = cterm_of Sign.pure (Var(("x",0),TVar(("'a",0),["logic"])))
+  let val cx = cterm_of Sign.pure (Var(("x",0),TVar(("'a",0),logicS)))
   in Thm.reflexive cx end;
 
 val symmetric_thm =
@@ -542,7 +545,7 @@
 val triv_forall_equality =
   let val V  = read_cterm Sign.pure ("PROP V", propT)
       and QV = read_cterm Sign.pure ("!!x::'a. PROP V", propT)
-      and x  = read_cterm Sign.pure ("x", TFree("'a",["logic"]));
+      and x  = read_cterm Sign.pure ("x", TFree("'a",logicS));
   in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
                            (implies_intr V  (forall_intr x (assume V))))
   end;