diff -r adf0eff5ea62 -r 87d1bddcdfe7 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon Nov 26 23:24:27 2001 +0100
+++ b/src/HOL/Tools/record_package.ML	Tue Nov 27 13:28:26 2001 +0100
@@ -83,7 +83,7 @@
 
 (* attributes *)
 
-val case_names_fields = RuleCases.case_names ["fields"];
+fun case_names_fields x = RuleCases.case_names ["fields"] x;
 fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name];
 fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name];