def_sort;
authorwenzelm
Sat Jun 20 20:35:38 1998 +0200 (1998-06-20)
changeset 50607b86df67cc1a
parent 5059 dcdb21e53537
child 5061 f947332d5465
def_sort;
src/HOL/Tools/record_package.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Sat Jun 20 20:18:51 1998 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Sat Jun 20 20:35:38 1998 +0200
     1.3 @@ -593,9 +593,9 @@
     1.4  
     1.5  fun read_typ sign (env, s) =
     1.6    let
     1.7 -    fun def_type (x, ~1) = assoc (env, x)
     1.8 -      | def_type _ = None;
     1.9 -    val T = Type.no_tvars (Sign.read_typ (sign, def_type) s) handle TYPE (msg, _, _) => error msg;
    1.10 +    fun def_sort (x, ~1) = assoc (env, x)
    1.11 +      | def_sort _ = None;
    1.12 +    val T = Type.no_tvars (Sign.read_typ (sign, def_sort) s) handle TYPE (msg, _, _) => error msg;
    1.13    in (Term.add_typ_tfrees (T, env), T) end;
    1.14  
    1.15  fun cert_typ sign (env, raw_T) =