src/Pure/pattern.ML
changeset 1501 bb7f99a0a6f0
parent 1460 5a6f2aabd538
child 1576 af8f43f742a0
     1.1 --- a/src/Pure/pattern.ML	Fri Feb 16 12:19:47 1996 +0100
     1.2 +++ b/src/Pure/pattern.ML	Fri Feb 16 12:34:18 1996 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  *)
     1.5  
     1.6  signature PATTERN =
     1.7 -sig
     1.8 +  sig
     1.9    type type_sig
    1.10    type sg
    1.11    type env
    1.12 @@ -25,13 +25,11 @@
    1.13    exception Unif
    1.14    exception MATCH
    1.15    exception Pattern
    1.16 -end;
    1.17 +  end;
    1.18  
    1.19 -functor PatternFun(structure Sign:SIGN and Envir:ENVIR): PATTERN =
    1.20 +structure Pattern : PATTERN =
    1.21  struct
    1.22  
    1.23 -structure Type = Sign.Type;
    1.24 -
    1.25  type type_sig = Type.type_sig
    1.26  type sg = Sign.sg
    1.27  type env = Envir.env