src/HOL/Tools/record.ML
changeset 33368 b1cf34f1855c
parent 33095 bbd52d2f8696
child 33385 fb2358edcfb6
     1.1 --- a/src/HOL/Tools/record.ML	Fri Oct 30 18:33:21 2009 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sun Nov 01 15:24:45 2009 +0100
     1.3 @@ -1553,7 +1553,7 @@
     1.4  
     1.5  (* attributes *)
     1.6  
     1.7 -fun case_names_fields x = RuleCases.case_names ["fields"] x;
     1.8 +fun case_names_fields x = Rule_Cases.case_names ["fields"] x;
     1.9  fun induct_type_global name = [case_names_fields, Induct.induct_type name];
    1.10  fun cases_type_global name = [case_names_fields, Induct.cases_type name];
    1.11