diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/context.ML
--- a/src/Pure/context.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/context.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -31,7 +31,6 @@
   type theory_id
   val theory_id: theory -> theory_id
   val timing: bool Unsynchronized.ref
-  type pretty
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val theory_id_name: theory_id -> string
@@ -52,7 +51,7 @@
   val subthy_id: theory_id * theory_id -> bool
   val subthy: theory * theory -> bool
   val finish_thy: theory -> theory
-  val begin_thy: (theory -> pretty) -> string -> theory list -> theory
+  val begin_thy: string -> theory list -> theory
   (*proof context*)
   val raw_transfer: theory -> Proof.context -> Proof.context
   (*certificate*)
@@ -77,11 +76,6 @@
   val proof_map: (generic -> generic) -> Proof.context -> Proof.context
   val theory_of: generic -> theory  (*total*)
   val proof_of: generic -> Proof.context  (*total*)
-  (*pretty printing context*)
-  val pretty: Proof.context -> pretty
-  val pretty_global: theory -> pretty
-  val pretty_generic: generic -> pretty
-  val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
   (*thread data*)
   val thread_data: unit -> generic option
   val the_thread_data: unit -> generic
@@ -97,7 +91,7 @@
   structure Theory_Data:
   sig
     val declare: Position.T -> Any.T -> (Any.T -> Any.T) ->
-      (pretty -> Any.T * Any.T -> Any.T) -> serial
+      (theory * theory -> Any.T * Any.T -> Any.T) -> serial
     val get: serial -> (Any.T -> 'a) -> theory -> 'a
     val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
   end
@@ -114,55 +108,9 @@
 
 (*** theory context ***)
 
-(** theory data **)
-
-(* data kinds and access methods *)
-
-val timing = Unsynchronized.ref false;
-
 (*private copy avoids potential conflict of table exceptions*)
 structure Datatab = Table(type key = int val ord = int_ord);
 
-datatype pretty = Pretty of Any.T;
-
-local
-
-type kind =
- {pos: Position.T,
-  empty: Any.T,
-  extend: Any.T -> Any.T,
-  merge: pretty -> Any.T * Any.T -> Any.T};
-
-val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
-
-fun invoke name f k x =
-  (case Datatab.lookup (Synchronized.value kinds) k of
-    SOME kind =>
-      if ! timing andalso name <> "" then
-        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
-          (fn () => f kind x)
-      else f kind x
-  | NONE => raise Fail "Invalid theory data identifier");
-
-in
-
-fun invoke_empty k = invoke "" (K o #empty) k ();
-val invoke_extend = invoke "extend" #extend;
-fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
-
-fun declare_theory_data pos empty extend merge =
-  let
-    val k = serial ();
-    val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
-    val _ = Synchronized.change kinds (Datatab.update (k, kind));
-  in k end;
-
-val extend_data = Datatab.map invoke_extend;
-fun merge_data pp = Datatab.join (invoke_merge pp) o apply2 extend_data;
-
-end;
-
-
 
 (** datatype theory **)
 
@@ -288,6 +236,51 @@
 
 
 
+(** theory data **)
+
+(* data kinds and access methods *)
+
+val timing = Unsynchronized.ref false;
+
+local
+
+type kind =
+ {pos: Position.T,
+  empty: Any.T,
+  extend: Any.T -> Any.T,
+  merge: theory * theory -> Any.T * Any.T -> Any.T};
+
+val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
+
+fun invoke name f k x =
+  (case Datatab.lookup (Synchronized.value kinds) k of
+    SOME kind =>
+      if ! timing andalso name <> "" then
+        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
+          (fn () => f kind x)
+      else f kind x
+  | NONE => raise Fail "Invalid theory data identifier");
+
+in
+
+fun invoke_empty k = invoke "" (K o #empty) k ();
+val invoke_extend = invoke "extend" #extend;
+fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
+
+fun declare_theory_data pos empty extend merge =
+  let
+    val k = serial ();
+    val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
+    val _ = Synchronized.change kinds (Datatab.update (k, kind));
+  in k end;
+
+val extend_data = Datatab.map invoke_extend;
+fun merge_data thys = Datatab.join (invoke_merge thys) o apply2 extend_data;
+
+end;
+
+
+
 (** build theories **)
 
 (* primitives *)
@@ -325,12 +318,12 @@
 
 local
 
-fun merge_thys pp (thy1, thy2) =
+fun merge_thys (thy1, thy2) =
   let
     val ids = merge_ids thy1 thy2;
     val history = make_history "" 0;
     val ancestry = make_ancestry [] [];
-    val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
+    val data = merge_data (thy1, thy2) (data_of thy1, data_of thy2);
   in create_thy ids history ancestry data end;
 
 fun maximal_thys thys =
@@ -338,7 +331,7 @@
 
 in
 
-fun begin_thy pp name imports =
+fun begin_thy name imports =
   if name = "" then error ("Bad theory name: " ^ quote name)
   else
     let
@@ -351,7 +344,7 @@
         (case parents of
           [] => error "Missing theory imports"
         | [thy] => extend_thy thy
-        | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
+        | thy :: thys => Library.foldl merge_thys (thy, thys));
 
       val history = make_history name 0;
       val ancestry = make_ancestry parents ancestors;
@@ -498,17 +491,6 @@
 val proof_of = cases Proof_Context.init_global I;
 
 
-(* pretty printing context *)
-
-exception PRETTY of generic;
-
-val pretty_generic = Pretty o PRETTY;
-val pretty = pretty_generic o Proof;
-val pretty_global = pretty_generic o Theory;
-
-fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
-
-
 
 (** thread data **)
 
@@ -551,12 +533,12 @@
 
 (** theory data **)
 
-signature THEORY_DATA_PP_ARGS =
+signature THEORY_DATA'_ARGS =
 sig
   type T
   val empty: T
   val extend: T -> T
-  val merge: Context.pretty -> T * T -> T
+  val merge: theory * theory -> T * T -> T
 end;
 
 signature THEORY_DATA_ARGS =
@@ -575,7 +557,7 @@
   val map: (T -> T) -> theory -> theory
 end;
 
-functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
+functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA =
 struct
 
 type T = Data.T;
@@ -586,7 +568,7 @@
     (Position.thread_data ())
     (Data Data.empty)
     (fn Data x => Data (Data.extend x))
-    (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
+    (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2)));
 
 val get = Context.Theory_Data.get kind (fn Data x => x);
 val put = Context.Theory_Data.put kind Data;
@@ -595,7 +577,7 @@
 end;
 
 functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
-  Theory_Data_PP
+  Theory_Data'
   (
     type T = Data.T;
     val empty = Data.empty;