eliminated odd object-oriented type_context/term_context;
export ProofContext.intern_skolem;

--- a/src/Pure/Isar/proof_context.ML	Wed Apr 06 14:44:40 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 06 15:10:39 2011 +0200
@@ -64,14 +64,11 @@
   val read_const_proper: Proof.context -> bool -> string -> term
   val read_const: Proof.context -> bool -> typ -> string -> term
   val allow_dummies: Proof.context -> Proof.context
+  val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
   val check_tvar: Proof.context -> indexname * sort -> indexname * sort
   val check_tfree: Proof.context -> string * sort -> string * sort
-  val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
-  type type_context
-  val type_context: Proof.context -> type_context
-  type term_context
-  val term_context: Proof.context -> term_context
   val standard_infer_types: Proof.context -> term list -> term list
+  val intern_skolem: Proof.context -> string -> string option
   val read_term_pattern: Proof.context -> string -> term
   val read_term_schematic: Proof.context -> string -> term
   val read_term_abbrev: Proof.context -> string -> term
@@ -266,7 +263,6 @@
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
 
 val consts_of = #1 o #consts o rep_context;
-val const_space = Consts.space_of o consts_of;
 val the_const_constraint = Consts.the_constraint o consts_of;
 
 val facts_of = #facts o rep_context;
@@ -526,6 +522,22 @@
 end;
 
 
+(* skolem variables *)
+
+fun intern_skolem ctxt x =
+  let
+    val _ = no_skolem false x;
+    val sko = lookup_skolem ctxt x;
+    val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
+    val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
+  in
+    if Variable.is_const ctxt x then NONE
+    else if is_some sko then sko
+    else if not is_const orelse is_declared then SOME x
+    else NONE
+  end;
+
+
 (* read_term *)
 
 fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt);
@@ -618,9 +630,7 @@
 end;
 
 
-(* decoding raw terms (syntax trees) *)
-
-(* types *)
+(* sort constraints *)
 
 fun get_sort ctxt raw_text =
   let
@@ -653,54 +663,6 @@
 fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
 fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
 
-local
-
-fun intern_skolem ctxt def_type x =
-  let
-    val _ = no_skolem false x;
-    val sko = lookup_skolem ctxt x;
-    val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
-    val is_declared = is_some (def_type (x, ~1));
-  in
-    if Variable.is_const ctxt x then NONE
-    else if is_some sko then sko
-    else if not is_const orelse is_declared then SOME x
-    else NONE
-  end;
-
-in
-
-type type_context =
- {get_class: string -> string,
-  get_type: string -> string,
-  markup_class: string -> Markup.T list,
-  markup_type: string -> Markup.T list};
-
-fun type_context ctxt : type_context =
- {get_class = read_class ctxt,
-  get_type = #1 o dest_Type o read_type_name_proper ctxt false,
-  markup_class = fn c => [Name_Space.markup_entry (Type.class_space (tsig_of ctxt)) c],
-  markup_type = fn c => [Name_Space.markup_entry (Type.type_space (tsig_of ctxt)) c]};
-
-type term_context =
- {get_const: string -> bool * string,
-  get_free: string -> string option,
-  markup_const: string -> Markup.T list,
-  markup_free: string -> Markup.T list,
-  markup_var: indexname -> Markup.T list};
-
-fun term_context ctxt : term_context =
- {get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
-    handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
-  get_free = intern_skolem ctxt (Variable.def_type ctxt false),
-  markup_const = fn c => [Name_Space.markup_entry (const_space ctxt) c],
-  markup_free = fn x =>
-    [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
-    (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]),
-  markup_var = fn xi => [Markup.name (Term.string_of_vname xi) Markup.var]};
-
-end;
-
 
 (* certify terms *)
 

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 14:44:40 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 15:10:39 2011 +0200
@@ -93,7 +93,12 @@
 
 fun parsetree_to_ast ctxt constrain_pos trf parsetree =
   let
-    val {get_class, get_type, markup_class, markup_type} = ProofContext.type_context ctxt;
+    val tsig = ProofContext.tsig_of ctxt;
+
+    val get_class = ProofContext.read_class ctxt;
+    val get_type = #1 o dest_Type o ProofContext.read_type_name_proper ctxt false;
+    fun markup_class c = [Name_Space.markup_entry (Type.class_space tsig) c];
+    fun markup_type c = [Name_Space.markup_entry (Type.type_space tsig) c];
 
     val reports = Unsynchronized.ref ([]: Position.reports);
     fun report pos = Position.reports reports [pos];
@@ -146,14 +151,23 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
-fun markup_bound def id =
-  [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
-
 fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
   | decode_term ctxt (reports0, Exn.Result tm) =
       let
-        val {get_const, get_free, markup_const, markup_free, markup_var} =
-          ProofContext.term_context ctxt;
+        val consts = ProofContext.consts_of ctxt;
+        fun get_const a =
+          ((true, #1 (Term.dest_Const (ProofContext.read_const_proper ctxt false a)))
+            handle ERROR _ => (false, Consts.intern consts a));
+        val get_free = ProofContext.intern_skolem ctxt;
+        fun markup_const c = [Name_Space.markup_entry (Consts.space_of consts) c];
+        fun markup_free x =
+          [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
+          (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then []
+           else [Markup.hilite]);
+        fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
+        fun markup_bound def id =
+          [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
+
         val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm));
 
         val reports = Unsynchronized.ref reports0;