src/Pure/consts.ML
changeset 35554 1e05ea0a5cd7
parent 35262 9ea4445d2ccf
child 35680 897740382442
     1.1 --- a/src/Pure/consts.ML	Wed Mar 03 20:45:48 2010 +0100
     1.2 +++ b/src/Pure/consts.ML	Wed Mar 03 22:50:35 2010 +0100
     1.3 @@ -21,8 +21,9 @@
     1.4    val space_of: T -> Name_Space.T
     1.5    val is_concealed: T -> string -> bool
     1.6    val intern: T -> xstring -> string
     1.7 +  val extern: T -> string -> xstring
     1.8    val intern_syntax: T -> xstring -> string
     1.9 -  val extern: T -> string -> xstring
    1.10 +  val extern_syntax: T -> string -> xstring
    1.11    val read_const: T -> string -> term
    1.12    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    1.13    val typargs: T -> string * typ -> typ list
    1.14 @@ -126,10 +127,15 @@
    1.15  val intern = Name_Space.intern o space_of;
    1.16  val extern = Name_Space.extern o space_of;
    1.17  
    1.18 -fun intern_syntax consts name =
    1.19 -  (case try Syntax.unmark_const name of
    1.20 +fun intern_syntax consts s =
    1.21 +  (case try Syntax.unmark_const s of
    1.22      SOME c => c
    1.23 -  | NONE => intern consts name);
    1.24 +  | NONE => intern consts s);
    1.25 +
    1.26 +fun extern_syntax consts s =
    1.27 +  (case try Syntax.unmark_const s of
    1.28 +    SOME c => extern consts c
    1.29 +  | NONE => s);
    1.30  
    1.31  
    1.32  (* read_const *)