| changeset 922 | 196ca0973a6d |
| parent 651 | 4b0455fbcc49 |
| child 1435 | aefcd255ed4a |
--- a/src/Pure/unify.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/unify.ML Fri Mar 03 11:48:05 1995 +0100 @@ -53,7 +53,7 @@ and trace_types = ref false (*announce potential incompleteness of type unification*) -val sgr = ref(Sign.pure); +val sgr = ref(Sign.proto_pure); type binderlist = (string*typ) list;