changeset 24713 | 8b3b6d09ef40 |
parent 24434 | c588ec4cf194 |
child 24770 | 695a8e087b9f |
--- a/src/Pure/pure_thy.ML Tue Sep 25 17:06:14 2007 +0200 +++ b/src/Pure/pure_thy.ML Tue Sep 25 17:06:18 2007 +0200 @@ -147,7 +147,7 @@ (** dataype theorems **) structure TheoremsData = TheoryDataFun -(struct +( type T = {theorems: thm list NameSpace.table, index: FactIndex.T} ref; @@ -159,7 +159,7 @@ fun copy (ref x) = ref x; val extend = mk_empty; fun merge _ = mk_empty; -end); +); val get_theorems_ref = TheoremsData.get; val get_theorems = ! o get_theorems_ref;