# HG changeset patch # User wenzelm # Date 1394383420 -3600 # Node ID 2897b2a4f7fdbc08a3153b3f9acad332810bd0b1 # Parent 1b61dfbcf9a4a6b26fa2511ab8b0c79c5bc0d3ed unused; diff -r 1b61dfbcf9a4 -r 2897b2a4f7fd src/Pure/consts.ML --- a/src/Pure/consts.ML Sun Mar 09 17:40:02 2014 +0100 +++ b/src/Pure/consts.ML Sun Mar 09 17:43:40 2014 +0100 @@ -22,9 +22,7 @@ val alias: Name_Space.naming -> binding -> string -> T -> T val is_concealed: T -> string -> bool val intern: T -> xstring -> string - val extern: Proof.context -> T -> string -> xstring val intern_syntax: T -> xstring -> string - val extern_syntax: Proof.context -> T -> string -> xstring val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*) val typargs: T -> string * typ -> typ list @@ -128,18 +126,12 @@ val is_concealed = Name_Space.is_concealed o space_of; val intern = Name_Space.intern o space_of; -fun extern ctxt = Name_Space.extern ctxt o space_of; fun intern_syntax consts s = (case try Lexicon.unmark_const s of SOME c => c | NONE => intern consts s); -fun extern_syntax ctxt consts s = - (case try Lexicon.unmark_const s of - SOME c => extern ctxt consts c - | NONE => s); - (* check_const *) diff -r 1b61dfbcf9a4 -r 2897b2a4f7fd src/Pure/type.ML --- a/src/Pure/type.ML Sun Mar 09 17:40:02 2014 +0100 +++ b/src/Pure/type.ML Sun Mar 09 17:43:40 2014 +0100 @@ -28,8 +28,6 @@ val empty_tsig: tsig val class_space: tsig -> Name_Space.T val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig - val intern_class: tsig -> xstring -> string - val extern_class: Proof.context -> tsig -> string -> xstring val defaultS: tsig -> sort val logical_types: tsig -> string list val eq_sort: tsig -> sort * sort -> bool @@ -49,8 +47,6 @@ val restore_mode: Proof.context -> Proof.context -> Proof.context val type_space: tsig -> Name_Space.T val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig - val intern_type: tsig -> xstring -> string - val extern_type: Proof.context -> tsig -> string -> xstring val is_logtype: tsig -> string -> bool val check_decl: Context.generic -> tsig -> xstring * Position.T -> (string * Position.report list) * decl @@ -200,9 +196,6 @@ fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) => ((Name_Space.alias naming binding name space, classes), default, types)); -val intern_class = Name_Space.intern o class_space; -fun extern_class ctxt = Name_Space.extern ctxt o class_space; - fun defaultS (TSig {default, ...}) = default; fun logical_types (TSig {log_types, ...}) = log_types; @@ -249,9 +242,6 @@ fun type_alias naming binding name = map_tsig (fn (classes, default, (space, types)) => (classes, default, (Name_Space.alias naming binding name space, types))); -val intern_type = Name_Space.intern o type_space; -fun extern_type ctxt = Name_Space.extern ctxt o type_space; - val is_logtype = member (op =) o logical_types;