| changeset 32734 | 06c13b2e562e |
| parent 32199 | 82c4c570310a |
| child 32740 | 9dd0a2f83429 |
--- a/src/Tools/coherent.ML Mon Sep 28 22:47:34 2009 +0200 +++ b/src/Tools/coherent.ML Mon Sep 28 23:13:37 2009 +0200 @@ -26,7 +26,7 @@ val setup: theory -> theory end; -functor CoherentFun(Data: COHERENT_DATA) : COHERENT = +functor Coherent(Data: COHERENT_DATA) : COHERENT = struct (** misc tools **)