src/HOL/Tools/inductive_package.ML
changeset 9201 435fef035d7f
parent 9116 9df44b5c610b
child 9235 1f734dc2e526
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Jun 29 22:37:24 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Jun 29 22:38:30 2000 +0200
     1.3 @@ -506,7 +506,7 @@
     1.4              (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops;
     1.5          in
     1.6            thy |> IsarThy.have_theorems_i
     1.7 -            (((name, atts), map Thm.no_attributes thms), comment)
     1.8 +            [(((name, atts), map Thm.no_attributes thms), comment)]
     1.9          end)
    1.10    end;
    1.11