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