src/Pure/display.ML
changeset 3990 a8c80f5fdd16
parent 3936 1954255c29ef
child 4126 c41846a38e20
     1.1 --- a/src/Pure/display.ML	Fri Oct 24 17:12:09 1997 +0200
     1.2 +++ b/src/Pure/display.ML	Fri Oct 24 17:12:35 1997 +0200
     1.3 @@ -103,16 +103,17 @@
     1.4  
     1.5  fun print_thy thy =
     1.6    let
     1.7 -    val {sign, new_axioms, oracles, ...} = rep_theory thy;
     1.8 -    val axioms = Symtab.dest new_axioms;
     1.9 +    val {sign, axioms, oracles, ...} = rep_theory thy;
    1.10 +    val axioms = Symtab.dest axioms;
    1.11      val oras = map fst (Symtab.dest oracles);
    1.12  
    1.13      fun prt_axm (a, t) = Pretty.block
    1.14 -      [Pretty.str (Sign.cond_extern sign Theory.thmK a ^ ":"), Pretty.brk 1,
    1.15 +      [Pretty.str (Sign.cond_extern sign Theory.axiomK a ^ ":"), Pretty.brk 1,
    1.16          Pretty.quote (Sign.pretty_term sign t)];
    1.17    in
    1.18 -    Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms));
    1.19 -    Pretty.writeln (Pretty.strs ("oracles:" :: oras))
    1.20 +    Pretty.writeln (Pretty.big_list "axioms:" (map prt_axm axioms));
    1.21 +    Pretty.writeln (Pretty.strs ("oracles:" :: oras));
    1.22 +    print_data thy "theorems"
    1.23    end;
    1.24  
    1.25  fun print_theory thy = (Sign.print_sg (sign_of thy); print_thy thy);
    1.26 @@ -134,7 +135,7 @@
    1.27          if x = x' then (x', y ins ys') :: pairs
    1.28          else pair :: ins_entry (x, y) pairs;
    1.29  
    1.30 -  fun add_consts (Const (c, T), env) = ins_entry (T, c) env
    1.31 +  fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
    1.32      | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
    1.33      | add_consts (Abs (_, _, t), env) = add_consts (t, env)
    1.34      | add_consts (_, env) = env;
    1.35 @@ -152,12 +153,12 @@
    1.36    fun less_idx ((x, i):indexname, (y, j):indexname) =
    1.37      x < y orelse x = y andalso i < j;
    1.38    fun sort_idxs l = map (apsnd (sort less_idx)) l;
    1.39 -  fun sort_strs l = map (apsnd sort_strings) l;
    1.40 +  fun sort_cnsts l = map (apsnd (sort_wrt fst)) l;
    1.41  
    1.42  
    1.43    (* prepare atoms *)
    1.44  
    1.45 -  fun consts_of t = sort_strs (add_consts (t, []));
    1.46 +  fun consts_of t = sort_cnsts (add_consts (t, []));
    1.47    fun vars_of t = sort_idxs (add_vars (t, []));
    1.48    fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
    1.49  
    1.50 @@ -183,7 +184,7 @@
    1.51        fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
    1.52          | prt_varT xi = prt_typ (TVar (xi, []));
    1.53  
    1.54 -      val prt_consts = prt_atoms (prt_term o Syntax.const) prt_typ;
    1.55 +      val prt_consts = prt_atoms (prt_term o Const) prt_typ;
    1.56        val prt_vars = prt_atoms prt_var prt_typ;
    1.57        val prt_varsT = prt_atoms prt_varT prt_sort;
    1.58