changeset 60825 | bacfb7c45d81 |
parent 60801 | 7664e0916eec |
child 61268 | abe08fb15a12 |
--- a/src/HOL/Tools/choice_specification.ML Tue Jul 28 21:31:16 2015 +0200 +++ b/src/HOL/Tools/choice_specification.ML Tue Jul 28 21:47:03 2015 +0200 @@ -178,7 +178,7 @@ else () in arg - |> apsnd Thm.unvarify_global + |> apsnd (Thm.unvarify_global thy) |> process_all (zip3 alt_names rew_imps frees) end