# HG changeset patch
# User wenzelm
# Date 1194529890 -3600
# Node ID dd5b851f8ef028184ad7fa947bb0440acef3641c
# Parent  00c2179db7698a58c192bbeb462f5b24c3f077c0
renamed ProofContext.read_const' to ProofContext.read_const_proper;
export expand_abbrevs;

diff -r 00c2179db769 -r dd5b851f8ef0 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Nov 08 14:51:29 2007 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Nov 08 14:51:30 2007 +0100
@@ -55,12 +55,13 @@
   val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
   val read_tyname: Proof.context -> string -> typ
-  val read_const': Proof.context -> string -> term
+  val read_const_proper: Proof.context -> string -> term
   val read_const: Proof.context -> string -> term
   val decode_term: Proof.context -> term -> term
   val read_term_pattern: Proof.context -> string -> term
   val read_term_schematic: Proof.context -> string -> term
   val read_term_abbrev: Proof.context -> string -> term
+  val expand_abbrevs: Proof.context -> term -> term
   val read_termTs_schematic: Proof.context -> (string -> bool) -> (indexname -> typ option)
     -> (indexname -> sort option) -> string list -> (string * typ) list
     -> term list * (indexname * typ) list
@@ -415,7 +416,7 @@
       val d = Sign.intern_type thy c;
     in Type (d, replicate (Sign.arity_number thy d) dummyT) end;
 
-fun read_const' ctxt c =
+fun read_const_proper ctxt c =
   (case Variable.lookup_const ctxt c of
     SOME d => Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => error msg)
   | NONE => Consts.read_const (consts_of ctxt) c);
@@ -423,7 +424,7 @@
 fun read_const ctxt c =
   (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
     (SOME x, false) => Free (x, infer_type ctxt x)
-  | _ => read_const' ctxt c);
+  | _ => read_const_proper ctxt c);
 
 
 (* read_term *)
@@ -512,7 +513,7 @@
 fun legacy_intern_skolem ctxt internal def_type x =    (* FIXME cleanup this mess *)
   let
     val sko = lookup_skolem ctxt x;
-    val is_const = can (read_const' ctxt) x;
+    val is_const = can (read_const_proper ctxt) x;
     val is_scoped_const = Variable.is_const ctxt x;
     val is_free = (is_some sko orelse not is_const) andalso not is_scoped_const;
     val is_internal = internal x;
@@ -530,7 +531,7 @@
 fun term_context ctxt =
   let val thy = theory_of ctxt in
    {get_sort = Sign.get_sort thy (Variable.def_sort ctxt),
-    map_const = try (#1 o Term.dest_Const o read_const' ctxt),
+    map_const = try (#1 o Term.dest_Const o read_const_proper ctxt),
     map_free = legacy_intern_skolem ctxt (K false) (Variable.def_type ctxt false),
     map_type = Sign.intern_tycons thy,
     map_sort = Sign.intern_sort thy}
@@ -986,7 +987,7 @@
 
 fun const_ast_tr intern ctxt [Syntax.Variable c] =
       let
-        val Const (c', _) = read_const' ctxt c;
+        val Const (c', _) = read_const_proper ctxt c;
         val d = if intern then const_syntax_name ctxt c' else c;
       in Syntax.Constant d end
   | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);