changeset 1500 | b2de3b3277b8 |
parent 1460 | 5a6f2aabd538 |
child 1835 | 07eee14f5bd4 |
--- a/src/Pure/logic.ML Fri Feb 16 12:08:49 1996 +0100 +++ b/src/Pure/logic.ML Fri Feb 16 12:19:47 1996 +0100 @@ -49,12 +49,9 @@ val varify : term -> term end; -functor LogicFun (structure Unify: UNIFY and Net:NET): LOGIC = +structure Logic : LOGIC = struct -structure Sign = Unify.Sign; -structure Type = Sign.Type; - (*** Abstract syntax operations on the meta-connectives ***) (** equality **)