# HG changeset patch
# User paulson
# Date 959077829 -7200
# Node ID 1cf815412d78da2f2f1aca86eef6b01e134f0a9f
# Parent  0c7f90147f5da05a3d7826ff7737a6c2caed3f2d
eta-expanded to handle value polymorphism

diff -r 0c7f90147f5d -r 1cf815412d78 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue May 23 12:13:45 2000 +0200
+++ b/src/Pure/axclass.ML	Tue May 23 12:30:29 2000 +0200
@@ -379,7 +379,7 @@
 val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
 val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
 val read_simple_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.intern_class;
-val cert_simple_arity = prep_arity (K I) Sign.certify_sort (K I);
+fun cert_simple_arity arg = prep_arity (K I) Sign.certify_sort (K I) arg;
 
 
 (* old-style instance declarations *)
diff -r 0c7f90147f5d -r 1cf815412d78 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue May 23 12:13:45 2000 +0200
+++ b/src/Pure/sign.ML	Tue May 23 12:30:29 2000 +0200
@@ -781,8 +781,8 @@
 fun ext_defS prep_sort (syn, tsig, ctab, (path, spaces), data) S =
   (syn, Type.ext_tsig_defsort tsig (prep_sort syn tsig spaces S), ctab, (path, spaces), data);
 
-val ext_defsort = ext_defS rd_sort;
-val ext_defsort_i = ext_defS cert_sort;
+fun ext_defsort arg   = ext_defS rd_sort arg;
+fun ext_defsort_i arg = ext_defS cert_sort arg;
 
 
 (* add type constructors *)
@@ -835,8 +835,8 @@
     (Syntax.extend_log_types syn log_types, tsig', ctab, (path, spaces), data)
   end;
 
-val ext_arities = ext_ars true rd_sort;
-val ext_arities_i = ext_ars false cert_sort;
+fun ext_arities arg   = ext_ars true rd_sort arg;
+fun ext_arities_i arg = ext_ars false cert_sort arg;
 
 
 (* add term constants and syntax *)