src/Pure/type.ML
changeset 59841 2551ac44150e
parent 59058 a78612c67ec0
child 59884 bbf49d7dfd6f
--- a/src/Pure/type.ML	Sun Mar 29 19:23:08 2015 +0200
+++ b/src/Pure/type.ML	Sun Mar 29 19:24:07 2015 +0200
@@ -49,7 +49,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 is_logtype: tsig -> string -> bool
   val check_decl: Context.generic -> tsig ->
     xstring * Position.T -> (string * Position.report list) * decl
   val the_decl: tsig -> string * Position.T -> decl
@@ -252,8 +251,6 @@
 fun type_alias naming binding name = map_tsig (fn (classes, default, types) =>
   (classes, default, (Name_Space.alias_table naming binding name types)));
 
-val is_logtype = member (op =) o logical_types;
-
 
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;