changeset 58956 | a816aa3ff391 |
parent 57949 | b203a7644bf1 |
child 59058 | a78612c67ec0 |
--- a/src/Tools/atomize_elim.ML Sun Nov 09 11:05:20 2014 +0100 +++ b/src/Tools/atomize_elim.ML Sun Nov 09 14:08:00 2014 +0100 @@ -120,7 +120,7 @@ val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis] @{thm meta_spec} in - compose_tac (false, rule, 1) i + compose_tac ctxt (false, rule, 1) i end in quantify_thesis