changeset 762 | baac4639ecef |
parent 760 | c1989de100b4 |
child 766 | df053507edba |
--- a/Quot/quotient_typ.ML Sat Dec 19 22:09:57 2009 +0100 +++ b/Quot/quotient_typ.ML Sat Dec 19 22:21:51 2009 +0100 @@ -1,4 +1,4 @@ -signature QUOTIENT = +signature QUOTIENT_TYPE = sig exception LIFT_MATCH of string @@ -7,9 +7,11 @@ end; -structure Quotient: QUOTIENT = +structure Quotient_Type: QUOTIENT_TYPE = struct +open Quotient_Info; + exception LIFT_MATCH of string (* wrappers for define, note, Attrib.internal and theorem_i *) @@ -223,4 +225,4 @@ end; (* structure *) -open Quotient +