Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/proofterm.ML
changeset 37216 3165bc303f66
parent 36883 4ed0d72def50
child 37236 739d8b9c59da 
--- a/src/Pure/proofterm.ML	Mon May 31 19:36:13 2010 +0200
+++ b/src/Pure/proofterm.ML	Mon May 31 21:06:57 2010 +0200
@@ -1328,7 +1328,7 @@
 
 (**** theory data ****)
 
-structure ProofData = Theory_Data
+structure Data = Theory_Data
 (
   type T =
     (stamp * (proof * proof)) list *
@@ -1341,11 +1341,11 @@
       AList.merge (op =) (K true) (procs1, procs2));
 );
 
-fun get_data thy = let val (rules, procs) = ProofData.get thy in (map #2 rules, map #2 procs) end;
+fun get_data thy = let val (rules, procs) = Data.get thy in (map #2 rules, map #2 procs) end;
 fun rew_proof thy = rewrite_prf fst (get_data thy);
 
-fun add_prf_rrule r = (ProofData.map o apfst) (cons (stamp (), r));
-fun add_prf_rproc p = (ProofData.map o apsnd) (cons (stamp (), p));
+fun add_prf_rrule r = (Data.map o apfst) (cons (stamp (), r));
+fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p));
 
 
 (***** promises *****)
isabelle