eta-expanded to handle value polymorphism
authorpaulson
Tue May 23 12:30:29 2000 +0200 (2000-05-23)
changeset 89271cf815412d78
parent 8926 0c7f90147f5d
child 8928 1d3bf47a4ecc
eta-expanded to handle value polymorphism
src/Pure/axclass.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/axclass.ML	Tue May 23 12:13:45 2000 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue May 23 12:30:29 2000 +0200
     1.3 @@ -379,7 +379,7 @@
     1.4  val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
     1.5  val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
     1.6  val read_simple_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.intern_class;
     1.7 -val cert_simple_arity = prep_arity (K I) Sign.certify_sort (K I);
     1.8 +fun cert_simple_arity arg = prep_arity (K I) Sign.certify_sort (K I) arg;
     1.9  
    1.10  
    1.11  (* old-style instance declarations *)
     2.1 --- a/src/Pure/sign.ML	Tue May 23 12:13:45 2000 +0200
     2.2 +++ b/src/Pure/sign.ML	Tue May 23 12:30:29 2000 +0200
     2.3 @@ -781,8 +781,8 @@
     2.4  fun ext_defS prep_sort (syn, tsig, ctab, (path, spaces), data) S =
     2.5    (syn, Type.ext_tsig_defsort tsig (prep_sort syn tsig spaces S), ctab, (path, spaces), data);
     2.6  
     2.7 -val ext_defsort = ext_defS rd_sort;
     2.8 -val ext_defsort_i = ext_defS cert_sort;
     2.9 +fun ext_defsort arg   = ext_defS rd_sort arg;
    2.10 +fun ext_defsort_i arg = ext_defS cert_sort arg;
    2.11  
    2.12  
    2.13  (* add type constructors *)
    2.14 @@ -835,8 +835,8 @@
    2.15      (Syntax.extend_log_types syn log_types, tsig', ctab, (path, spaces), data)
    2.16    end;
    2.17  
    2.18 -val ext_arities = ext_ars true rd_sort;
    2.19 -val ext_arities_i = ext_ars false cert_sort;
    2.20 +fun ext_arities arg   = ext_ars true rd_sort arg;
    2.21 +fun ext_arities_i arg = ext_ars false cert_sort arg;
    2.22  
    2.23  
    2.24  (* add term constants and syntax *)