| changeset 33519 | e31a85f92ce9 |
| parent 33314 | 53d49370f7af |
| child 33522 | 737589bb9bb8 |
--- a/src/Pure/Isar/code.ML Sun Nov 08 16:28:18 2009 +0100 +++ b/src/Pure/Isar/code.ML Sun Nov 08 16:30:41 2009 +0100 @@ -794,12 +794,12 @@ structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS = struct -structure Data = GenericDataFun +structure Data = Generic_Data ( type T = thm list; val empty = []; val extend = I; - fun merge _ = Thm.merge_thms; + val merge = Thm.merge_thms; ); val get = Data.get o Context.Proof;