| changeset 12302 | 87d1bddcdfe7 |
| parent 12265 | 6df58e87ec91 |
| child 12311 | ce5f9e61c037 |
--- 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];