author | wenzelm |
Tue, 27 Nov 2001 13:28:26 +0100 | |
changeset 12302 | 87d1bddcdfe7 |
parent 12301 | adf0eff5ea62 |
child 12303 | 67ca723a02dd |
--- 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];