| changeset 3991 | 4cb2f2422695 |
| parent 2753 | bcde71e5f371 |
| child 4270 | 957c887b89b5 |
--- a/src/Pure/unify.ML Fri Oct 24 17:12:35 1997 +0200 +++ b/src/Pure/unify.ML Fri Oct 24 17:13:21 1997 +0200 @@ -41,7 +41,7 @@ and trace_types = ref false (*announce potential incompleteness of type unification*) -val sgr = ref(Sign.proto_pure); +val sgr = ref(Sign.pre_pure); type binderlist = (string*typ) list;