# HG changeset patch
# User wenzelm
# Date 1301248311 -7200
# Node ID 4bc55652c685e362ad54ccb99f9bde3c8fe6658e
# Parent  74479999cf25a5dc3206cf04b6a970d5ce2298fd
tuned signatures;

diff -r 74479999cf25 -r 4bc55652c685 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Mar 27 19:27:31 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 27 19:51:51 2011 +0200
@@ -664,15 +664,13 @@
 
 in
 
-fun term_context ctxt =
+fun term_context ctxt : Syntax.term_context =
   {get_sort = get_sort ctxt,
-   map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
+   get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
      handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
-   map_free = intern_skolem ctxt (Variable.def_type ctxt false)};
+   get_free = intern_skolem ctxt (Variable.def_type ctxt false)};
 
-fun decode_term ctxt =
-  let val {get_sort, map_const, map_free} = term_context ctxt
-  in Syntax.decode_term get_sort map_const map_free end;
+val decode_term = Syntax.decode_term o term_context;
 
 end;
 
@@ -757,8 +755,6 @@
 
 fun parse_term T ctxt text =
   let
-    val {get_sort, map_const, map_free} = term_context ctxt;
-
     val (T', _) = Type_Infer.paramify_dummies T 0;
     val (markup, kind) =
       if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
@@ -775,9 +771,8 @@
     fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
       handle ERROR msg => SOME msg;
     val t =
-      Syntax.standard_parse_term check get_sort map_const map_free
-        ctxt (syn_of ctxt) root (syms, pos)
-      handle ERROR msg => parse_failed ctxt pos msg kind;
+      Syntax.standard_parse_term check (term_context ctxt) ctxt (syn_of ctxt) root (syms, pos)
+        handle ERROR msg => parse_failed ctxt pos msg kind;
   in t end;
 
 
diff -r 74479999cf25 -r 4bc55652c685 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Mar 27 19:27:31 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Mar 27 19:51:51 2011 +0200
@@ -116,10 +116,8 @@
   val ambiguity_level_raw: Config.raw
   val ambiguity_level: int Config.T
   val ambiguity_limit: int Config.T
-  val standard_parse_term: (term -> string option) ->
-    (((string * int) * sort) list -> string * int -> Term.sort) ->
-    (string -> bool * string) -> (string -> string option) -> Proof.context ->
-    syntax -> string -> Symbol_Pos.T list * Position.T -> term
+  val standard_parse_term: (term -> string option) -> term_context ->
+    Proof.context -> syntax -> string -> Symbol_Pos.T list * Position.T -> term
   val standard_parse_typ: Proof.context -> syntax ->
     ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
   val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
@@ -792,9 +790,9 @@
             map (show_term o snd) (take limit results)))
       end;
 
-fun standard_parse_term check get_sort map_const map_free ctxt syn root (syms, pos) =
+fun standard_parse_term check term_ctxt ctxt syn root (syms, pos) =
   read ctxt syn root (syms, pos)
-  |> map (Type_Ext.decode_term get_sort map_const map_free)
+  |> map (Type_Ext.decode_term term_ctxt)
   |> disambig ctxt check;
 
 
diff -r 74479999cf25 -r 4bc55652c685 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Sun Mar 27 19:27:31 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Sun Mar 27 19:51:51 2011 +0200
@@ -12,9 +12,8 @@
   val is_position: term -> bool
   val strip_positions: term -> term
   val strip_positions_ast: Ast.ast -> Ast.ast
-  val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
-    (string -> bool * string) -> (string -> string option) -> term ->
-    (Position.T * Markup.T) list * term
+  type term_context
+  val decode_term: term_context -> term -> (Position.T * Markup.T) list * term
   val term_of_typ: bool -> typ -> term
   val no_brackets: unit -> bool
   val no_type_brackets: unit -> bool
@@ -137,7 +136,12 @@
 fun markup_bound def id =
   Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound;
 
-fun decode_term get_sort map_const map_free tm =
+type term_context =
+ {get_sort: (indexname * sort) list -> indexname -> sort,
+  get_const: string -> bool * string,
+  get_free: string -> string option};
+
+fun decode_term ({get_sort, get_const, get_free}: term_context) tm =
   let
     val decodeT = typ_of_term (get_sort (term_sorts tm));
 
@@ -169,11 +173,11 @@
                 val c =
                   (case try Lexicon.unmark_const a of
                     SOME c => c
-                  | NONE => snd (map_const a));
+                  | NONE => snd (get_const a));
                 val _ = report ps markup_const c;
               in Const (c, T) end)
       | decode ps _ _ (Free (a, T)) =
-          (case (map_free a, map_const a) of
+          (case (get_free a, get_const a) of
             (SOME x, _) => (report ps markup_free x; Free (x, T))
           | (_, (true, c)) => (report ps markup_const c; Const (c, T))
           | (_, (false, c)) =>