changeset 74200 | 17090e27aae9 |
parent 70494 | 41108e3e9ca5 |
child 74266 | 612b7e0d6721 |
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Wed Aug 25 22:17:38 2021 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Thu Aug 26 14:45:19 2021 +0200 @@ -42,7 +42,7 @@ |> Conjunction.intr_balanced |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)] |> Thm.implies_intr assum - |> Thm.generalize ([], params) 0 + |> Thm.generalize (Symtab.empty, Symtab.make_set params) 0 |> Axclass.unoverload ctxt |> Thm.varifyT_global end;