src/Pure/theory.ML

--- a/src/Pure/theory.ML	Sat Sep 04 22:36:42 2010 +0200
+++ b/src/Pure/theory.ML	Sun Sep 05 19:47:40 2010 +0200
@@ -167,7 +167,7 @@
       error ("Illegal sort constraints in primitive specification: " ^
         commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
   in
-    (b, Sign.no_vars (Syntax.pp_global thy) t)
+    (b, Sign.no_vars (Syntax.init_pretty_global thy) t)
   end handle ERROR msg =>
     cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
 
@@ -182,10 +182,10 @@
 
 fun dependencies thy unchecked def description lhs rhs =
   let
-    val pp = Syntax.pp_global thy;
+    val ctxt = Syntax.init_pretty_global thy;
     val consts = Sign.consts_of thy;
     fun prep const =
-      let val Const (c, T) = Sign.no_vars pp (Const const)
+      let val Const (c, T) = Sign.no_vars ctxt (Const const)
       in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end;
 
     val lhs_vars = Term.add_tfreesT (#2 lhs) [];
@@ -194,9 +194,9 @@
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^
-        commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
+        commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
         "\nThe error(s) above occurred in " ^ quote description);
-  in Defs.define pp unchecked def description (prep lhs) (map prep rhs) end;
+  in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
 
 fun add_deps a raw_lhs raw_rhs thy =
   let