src/Pure/proofterm.ML
changeset 33522 737589bb9bb8
parent 33414 934801690991
child 33722 e588744f14da
     1.1 --- a/src/Pure/proofterm.ML	Sun Nov 08 18:43:22 2009 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Sun Nov 08 18:43:42 2009 +0100
     1.3 @@ -1247,14 +1247,13 @@
     1.4  
     1.5  (**** theory data ****)
     1.6  
     1.7 -structure ProofData = TheoryDataFun
     1.8 +structure ProofData = Theory_Data
     1.9  (
    1.10    type T = (stamp * (proof * proof)) list * (stamp * (typ list -> proof -> proof option)) list;
    1.11  
    1.12    val empty = ([], []);
    1.13 -  val copy = I;
    1.14    val extend = I;
    1.15 -  fun merge _ ((rules1, procs1), (rules2, procs2)) : T =
    1.16 +  fun merge ((rules1, procs1), (rules2, procs2)) : T =
    1.17      (AList.merge (op =) (K true) (rules1, rules2),
    1.18        AList.merge (op =) (K true) (procs1, procs2));
    1.19  );