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