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