changeset 52230 | 1105b3b5aa77 |
parent 51717 | 9e7d1c139569 |
child 52788 | da1fdbfebd39 |
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu May 30 08:27:51 2013 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu May 30 12:35:40 2013 +0200 @@ -51,7 +51,7 @@ in thms |> Conjunction.intr_balanced - |> Raw_Simplifier.rewrite_rule [Thm.symmetric (Thm.assume asm)] + |> rewrite_rule [Thm.symmetric (Thm.assume asm)] |> Thm.implies_intr asm |> Thm.generalize ([], params) 0 |> Axclass.unoverload thy