src/Pure/theory.ML
changeset 26939 1035c89b4c02
parent 26668 65023d4fd226
child 28017 4919bd124a58
     1.1 --- a/src/Pure/theory.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/Pure/theory.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -162,7 +162,7 @@
     1.4  
     1.5  fun begin_theory name imports =
     1.6    let
     1.7 -    val thy = Context.begin_thy Sign.pp name imports;
     1.8 +    val thy = Context.begin_thy Syntax.pp_global name imports;
     1.9      val wrappers = begin_wrappers thy;
    1.10    in thy |> Sign.local_path |> apply_wrappers wrappers end;
    1.11  
    1.12 @@ -185,7 +185,7 @@
    1.13          | TERM (msg, _) => error msg;
    1.14    in
    1.15      Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
    1.16 -    (name, Sign.no_vars (Sign.pp thy) t)
    1.17 +    (name, Sign.no_vars (Syntax.pp_global thy) t)
    1.18    end;
    1.19  
    1.20  fun read_axm thy (name, str) =
    1.21 @@ -219,7 +219,7 @@
    1.22  
    1.23  fun dependencies thy unchecked is_def name lhs rhs =
    1.24    let
    1.25 -    val pp = Sign.pp thy;
    1.26 +    val pp = Syntax.pp_global thy;
    1.27      val consts = Sign.consts_of thy;
    1.28      fun prep const =
    1.29        let val Const (c, T) = Sign.no_vars pp (Const const)
    1.30 @@ -256,7 +256,7 @@
    1.31  
    1.32      fun message txt =
    1.33        [Pretty.block [Pretty.str "Specification of constant ",
    1.34 -        Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ thy T)],
    1.35 +        Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ_global thy T)],
    1.36          Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
    1.37    in
    1.38      if Sign.typ_instance thy (declT, T') then ()
    1.39 @@ -281,7 +281,7 @@
    1.40    in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
    1.41    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    1.42     [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
    1.43 -    Pretty.fbrk, Pretty.quote (Sign.pretty_term thy tm)]));
    1.44 +    Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
    1.45  
    1.46  
    1.47  (* add_defs(_i) *)