# 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;