| changeset 18377 | 0e1d025d57b3 |
| parent 18011 | 685d95c793ff |
| child 18418 | bf448d999b7e |
--- a/src/Pure/Isar/context_rules.ML Thu Dec 08 20:16:17 2005 +0100 +++ b/src/Pure/Isar/context_rules.ML Fri Dec 09 09:06:45 2005 +0100 @@ -252,7 +252,7 @@ end; val _ = Context.add_setup - [#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]]; + [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]]; (* low-level modifiers *)