| changeset 18418 | bf448d999b7e |
| parent 18377 | 0e1d025d57b3 |
| child 18637 | 33a6f6caa617 |
--- a/src/Pure/Isar/context_rules.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/Pure/Isar/context_rules.ML Fri Dec 16 09:00:11 2005 +0100 @@ -258,7 +258,7 @@ (* low-level modifiers *) fun modifier att (x, ths) = - #1 (Thm.applys_attributes ((x, rev ths), [att])); + fst (Thm.applys_attributes [att] (x, rev ths)); val addXIs_global = modifier (intro_query_global NONE); val addXEs_global = modifier (elim_query_global NONE);