src/Pure/conjunction.ML
changeset 28674 08a77c495dc1
parent 26653 60e0cf6bef89
child 28856 5e009a80fe6d
     1.1 --- a/src/Pure/conjunction.ML	Thu Oct 23 14:22:16 2008 +0200
     1.2 +++ b/src/Pure/conjunction.ML	Thu Oct 23 15:28:01 2008 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4  val A_B = read_prop "A && B";
     1.5  
     1.6  val conjunction_def =
     1.7 -  Thm.unvarify (Thm.get_axiom (Context.the_theory (Context.the_thread_data ())) "conjunction_def");
     1.8 +  Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
     1.9  
    1.10  fun conjunctionD which =
    1.11    Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP