changeset 20260 | 990dbc007ca6 |
parent 20249 | a13adb4f94dc |
child 20508 | 8182d961c7cc |
--- a/src/Pure/conjunction.ML Sun Jul 30 21:28:51 2006 +0200 +++ b/src/Pure/conjunction.ML Sun Jul 30 21:28:52 2006 +0200 @@ -139,7 +139,7 @@ val B = Free ("B", propT); fun comp_rule th rule = - Thm.adjust_maxidx_thm (th COMP + Thm.adjust_maxidx_thm ~1 (th COMP (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1))); in