1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 06 14:44:40 2011 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 06 15:10:39 2011 +0200
     1.3 @@ -64,14 +64,11 @@
     1.4    val read_const_proper: Proof.context -> bool -> string -> term
     1.5    val read_const: Proof.context -> bool -> typ -> string -> term
     1.6    val allow_dummies: Proof.context -> Proof.context
     1.7 +  val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
     1.8    val check_tvar: Proof.context -> indexname * sort -> indexname * sort
     1.9    val check_tfree: Proof.context -> string * sort -> string * sort
    1.10 -  val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
    1.11 -  type type_context
    1.12 -  val type_context: Proof.context -> type_context
    1.13 -  type term_context
    1.14 -  val term_context: Proof.context -> term_context
    1.15    val standard_infer_types: Proof.context -> term list -> term list
    1.16 +  val intern_skolem: Proof.context -> string -> string option
    1.17    val read_term_pattern: Proof.context -> string -> term
    1.18    val read_term_schematic: Proof.context -> string -> term
    1.19    val read_term_abbrev: Proof.context -> string -> term
    1.20 @@ -266,7 +263,6 @@
    1.21  fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
    1.22  
    1.23  val consts_of = #1 o #consts o rep_context;
    1.24 -val const_space = Consts.space_of o consts_of;
    1.25  val the_const_constraint = Consts.the_constraint o consts_of;
    1.26  
    1.27  val facts_of = #facts o rep_context;
    1.28 @@ -526,6 +522,22 @@
    1.29  end;
    1.30  
    1.31  
    1.32 +(* skolem variables *)
    1.33 +
    1.34 +fun intern_skolem ctxt x =
    1.35 +  let
    1.36 +    val _ = no_skolem false x;
    1.37 +    val sko = lookup_skolem ctxt x;
    1.38 +    val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
    1.39 +    val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
    1.40 +  in
    1.41 +    if Variable.is_const ctxt x then NONE
    1.42 +    else if is_some sko then sko
    1.43 +    else if not is_const orelse is_declared then SOME x
    1.44 +    else NONE
    1.45 +  end;
    1.46 +
    1.47 +
    1.48  (* read_term *)
    1.49  
    1.50  fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt);
    1.51 @@ -618,9 +630,7 @@
    1.52  end;
    1.53  
    1.54  
    1.55 -(* decoding raw terms (syntax trees) *)
    1.56 -
    1.57 -(* types *)
    1.58 +(* sort constraints *)
    1.59  
    1.60  fun get_sort ctxt raw_text =
    1.61    let
    1.62 @@ -653,54 +663,6 @@
    1.63  fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
    1.64  fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
    1.65  
    1.66 -local
    1.67 -
    1.68 -fun intern_skolem ctxt def_type x =
    1.69 -  let
    1.70 -    val _ = no_skolem false x;
    1.71 -    val sko = lookup_skolem ctxt x;
    1.72 -    val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
    1.73 -    val is_declared = is_some (def_type (x, ~1));
    1.74 -  in
    1.75 -    if Variable.is_const ctxt x then NONE
    1.76 -    else if is_some sko then sko
    1.77 -    else if not is_const orelse is_declared then SOME x
    1.78 -    else NONE
    1.79 -  end;
    1.80 -
    1.81 -in
    1.82 -
    1.83 -type type_context =
    1.84 - {get_class: string -> string,
    1.85 -  get_type: string -> string,
    1.86 -  markup_class: string -> Markup.T list,
    1.87 -  markup_type: string -> Markup.T list};
    1.88 -
    1.89 -fun type_context ctxt : type_context =
    1.90 - {get_class = read_class ctxt,
    1.91 -  get_type = #1 o dest_Type o read_type_name_proper ctxt false,
    1.92 -  markup_class = fn c => [Name_Space.markup_entry (Type.class_space (tsig_of ctxt)) c],
    1.93 -  markup_type = fn c => [Name_Space.markup_entry (Type.type_space (tsig_of ctxt)) c]};
    1.94 -
    1.95 -type term_context =
    1.96 - {get_const: string -> bool * string,
    1.97 -  get_free: string -> string option,
    1.98 -  markup_const: string -> Markup.T list,
    1.99 -  markup_free: string -> Markup.T list,
   1.100 -  markup_var: indexname -> Markup.T list};
   1.101 -
   1.102 -fun term_context ctxt : term_context =
   1.103 - {get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
   1.104 -    handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
   1.105 -  get_free = intern_skolem ctxt (Variable.def_type ctxt false),
   1.106 -  markup_const = fn c => [Name_Space.markup_entry (const_space ctxt) c],
   1.107 -  markup_free = fn x =>
   1.108 -    [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
   1.109 -    (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]),
   1.110 -  markup_var = fn xi => [Markup.name (Term.string_of_vname xi) Markup.var]};
   1.111 -
   1.112 -end;
   1.113 -
   1.114  
   1.115  (* certify terms *)
   1.116