src/Pure/Thy/thm_database.ML
changeset 1512 ce37c64244c0
parent 1308 396ef8aa37b7
child 1580 e3fd931e6095
     1.1 --- a/src/Pure/Thy/thm_database.ML	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/src/Pure/Thy/thm_database.ML	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4                   indexed by the constants they contain*)
     1.5  
     1.6  signature THMDB =
     1.7 -sig
     1.8 +  sig
     1.9    val thm_db: thm_db_type ref
    1.10    val store_thm_db: string * thm -> thm
    1.11    val delete_thm_db: theory -> unit
    1.12 @@ -23,7 +23,7 @@
    1.13    val findI:         int -> (string * thm)list
    1.14    val findEs:        int -> (string * thm)list
    1.15    val findE:  int -> int -> (string * thm)list
    1.16 -end;
    1.17 +  end;
    1.18  
    1.19  functor ThmDBFun(): THMDB =
    1.20  struct