src/Pure/conjunction.ML
changeset 33277 1bdc3c732fdd
parent 32765 3032c0308019
child 33384 1b5ba4e6a953
     1.1 --- a/src/Pure/conjunction.ML	Wed Oct 28 16:25:10 2009 +0100
     1.2 +++ b/src/Pure/conjunction.ML	Wed Oct 28 16:25:26 2009 +0100
     1.3 @@ -83,15 +83,16 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1);
     1.8 -val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2);
     1.9 +val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1);
    1.10 +val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2);
    1.11  
    1.12 -val conjunctionI = Drule.store_standard_thm "conjunctionI"
    1.13 -  (Drule.implies_intr_list [A, B]
    1.14 -    (Thm.equal_elim
    1.15 -      (Thm.symmetric conjunction_def)
    1.16 -      (Thm.forall_intr C (Thm.implies_intr ABC
    1.17 -        (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
    1.18 +val conjunctionI =
    1.19 +  Drule.store_standard_thm (Binding.name "conjunctionI")
    1.20 +    (Drule.implies_intr_list [A, B]
    1.21 +      (Thm.equal_elim
    1.22 +        (Thm.symmetric conjunction_def)
    1.23 +        (Thm.forall_intr C (Thm.implies_intr ABC
    1.24 +          (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
    1.25  
    1.26  
    1.27  fun intr tha thb =