src/Pure/conjunction.ML
changeset 35845 e5980f0ad025
parent 33384 1b5ba4e6a953
child 35985 0bbf0d2348f9
     1.1 --- a/src/Pure/conjunction.ML	Sat Mar 20 02:23:41 2010 +0100
     1.2 +++ b/src/Pure/conjunction.ML	Sat Mar 20 17:33:11 2010 +0100
     1.3 @@ -75,7 +75,8 @@
     1.4  val A_B = read_prop "A &&& B";
     1.5  
     1.6  val conjunction_def =
     1.7 -  Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
     1.8 +  Thm.unvarify_global
     1.9 +    (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
    1.10  
    1.11  fun conjunctionD which =
    1.12    Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP