# HG changeset patch # User clasohm # Date 786887128 -3600 # Node ID d5a626aacdd32bcce338a795a259466b2b3b0262 # Parent 1cf9ebcc3ff379b19b60817dda29ed4130c500a4 replaced type_syn by pure_syn in Pure signature diff -r 1cf9ebcc3ff3 -r d5a626aacdd3 src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Dec 08 11:28:34 1994 +0100 +++ b/src/Pure/sign.ML Thu Dec 08 12:45:28 1994 +0100 @@ -512,7 +512,7 @@ (** the Pure signature **) val pure = - make_sign (Syntax.type_syn, tsig0, Symtab.null) [] "#" + make_sign (Syntax.pure_syn, tsig0, Symtab.null) [] "#" |> add_types (("fun", 2, NoSyn) :: ("prop", 0, NoSyn) ::