src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 33522 737589bb9bb8
parent 33316 6a72af4e84b8
child 33604 d4220df6fde2
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Nov 08 18:43:22 2009 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Nov 08 18:43:42 2009 +0100
     1.3 @@ -226,13 +226,12 @@
     1.4  
     1.5  fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
     1.6  
     1.7 -structure Provers = TheoryDataFun
     1.8 +structure Provers = Theory_Data
     1.9  (
    1.10    type T = (ATP_Wrapper.prover * stamp) Symtab.table;
    1.11    val empty = Symtab.empty;
    1.12 -  val copy = I;
    1.13    val extend = I;
    1.14 -  fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
    1.15 +  fun merge data : T = Symtab.merge (eq_snd op =) data
    1.16      handle Symtab.DUP dup => err_dup_prover dup;
    1.17  );
    1.18