1.1 --- a/src/Pure/display.ML	Wed Mar 17 16:32:38 1999 +0100
     1.2 +++ b/src/Pure/display.ML	Wed Mar 17 16:33:00 1999 +0100
     1.3 @@ -121,10 +121,10 @@
     1.4  
     1.5  (** print theory **)
     1.6  
     1.7 -val pretty_theory = Sign.pretty_sg o sign_of;
     1.8 -val pprint_theory = Sign.pprint_sg o sign_of;
     1.9 +val pretty_theory = Sign.pretty_sg o Theory.sign_of;
    1.10 +val pprint_theory = Sign.pprint_sg o Theory.sign_of;
    1.11  
    1.12 -val print_syntax = Syntax.print_syntax o syn_of;
    1.13 +val print_syntax = Syntax.print_syntax o Theory.syn_of;
    1.14  
    1.15  
    1.16  (* pretty_name_space  *)
    1.17 @@ -201,7 +201,7 @@
    1.18  
    1.19  fun print_thy thy =
    1.20    let
    1.21 -    val {sign, axioms, oracles, ...} = rep_theory thy;
    1.22 +    val {sign, axioms, oracles, ...} = Theory.rep_theory thy;
    1.23      val axioms = Symtab.dest axioms;
    1.24      val oras = map fst (Symtab.dest oracles);
    1.25  
    1.26 @@ -213,7 +213,7 @@
    1.27      Pretty.writeln (Pretty.strs ("oracles:" :: oras))
    1.28    end;
    1.29  
    1.30 -fun print_theory thy = (print_sign (sign_of thy); print_thy thy);
    1.31 +fun print_theory thy = (print_sign (Theory.sign_of thy); print_thy thy);
    1.32  
    1.33  (*also show consts in case of showing types?*)
    1.34  val show_consts = ref false;