src/Pure/theory.ML
changeset 22578 b0eb5652f210
parent 22485 3a7d623485fa
child 22600 043232f8dde2
     1.1 --- a/src/Pure/theory.ML	Wed Apr 04 00:10:59 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Wed Apr 04 00:11:03 2007 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  signature BASIC_THEORY =
     1.6  sig
     1.7 -  val sign_of: theory -> theory    (*obsolete*)
     1.8    val rep_theory: theory ->
     1.9     {axioms: term NameSpace.table,
    1.10      defs: Defs.T,
    1.11 @@ -85,8 +84,6 @@
    1.12  
    1.13  (* signature operations *)
    1.14  
    1.15 -val sign_of = I;
    1.16 -
    1.17  structure SignTheory: SIGN_THEORY = Sign;
    1.18  open SignTheory;
    1.19