src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
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;