src/Pure/theory.ML
changeset 22578 b0eb5652f210
parent 22485 3a7d623485fa
child 22600 043232f8dde2
--- a/src/Pure/theory.ML	Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Pure/theory.ML	Wed Apr 04 00:11:03 2007 +0200
@@ -7,7 +7,6 @@
 
 signature BASIC_THEORY =
 sig
-  val sign_of: theory -> theory    (*obsolete*)
   val rep_theory: theory ->
    {axioms: term NameSpace.table,
     defs: Defs.T,
@@ -85,8 +84,6 @@
 
 (* signature operations *)
 
-val sign_of = I;
-
 structure SignTheory: SIGN_THEORY = Sign;
 open SignTheory;