src/Pure/proofterm.ML
changeset 37216 3165bc303f66
parent 36883 4ed0d72def50
child 37236 739d8b9c59da
     1.1 --- a/src/Pure/proofterm.ML	Mon May 31 19:36:13 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Mon May 31 21:06:57 2010 +0200
     1.3 @@ -1328,7 +1328,7 @@
     1.4  
     1.5  (**** theory data ****)
     1.6  
     1.7 -structure ProofData = Theory_Data
     1.8 +structure Data = Theory_Data
     1.9  (
    1.10    type T =
    1.11      (stamp * (proof * proof)) list *
    1.12 @@ -1341,11 +1341,11 @@
    1.13        AList.merge (op =) (K true) (procs1, procs2));
    1.14  );
    1.15  
    1.16 -fun get_data thy = let val (rules, procs) = ProofData.get thy in (map #2 rules, map #2 procs) end;
    1.17 +fun get_data thy = let val (rules, procs) = Data.get thy in (map #2 rules, map #2 procs) end;
    1.18  fun rew_proof thy = rewrite_prf fst (get_data thy);
    1.19  
    1.20 -fun add_prf_rrule r = (ProofData.map o apfst) (cons (stamp (), r));
    1.21 -fun add_prf_rproc p = (ProofData.map o apsnd) (cons (stamp (), p));
    1.22 +fun add_prf_rrule r = (Data.map o apfst) (cons (stamp (), r));
    1.23 +fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p));
    1.24  
    1.25  
    1.26  (***** promises *****)