# HG changeset patch
# User wenzelm
# Date 898367738 -7200
# Node ID 7b86df67cc1a2855514711a6205364d902e983c8
# Parent  dcdb21e5353784989058bcb9fe00ebc747f53326
def_sort;

diff -r dcdb21e53537 -r 7b86df67cc1a src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sat Jun 20 20:18:51 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Sat Jun 20 20:35:38 1998 +0200
@@ -593,9 +593,9 @@
 
 fun read_typ sign (env, s) =
   let
-    fun def_type (x, ~1) = assoc (env, x)
-      | def_type _ = None;
-    val T = Type.no_tvars (Sign.read_typ (sign, def_type) s) handle TYPE (msg, _, _) => error msg;
+    fun def_sort (x, ~1) = assoc (env, x)
+      | def_sort _ = None;
+    val T = Type.no_tvars (Sign.read_typ (sign, def_sort) s) handle TYPE (msg, _, _) => error msg;
   in (Term.add_typ_tfrees (T, env), T) end;
 
 fun cert_typ sign (env, raw_T) =