changeset 42799 | 4e33894aec6d |
parent 42366 | 2305c70ec9b1 |
child 43333 | 2bdec7f430d3 |
--- a/src/Provers/hypsubst.ML Sat May 14 00:32:16 2011 +0200 +++ b/src/Provers/hypsubst.ML Sat May 14 11:42:43 2011 +0200 @@ -53,7 +53,7 @@ val hypsubst_setup : theory -> theory end; -functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = +functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST = struct exception EQ_VAR;