| changeset 29582 | 0950f4f0d0cd |
| parent 27809 | a1e409db516b |
| child 29606 | fedb8be05f24 |
--- a/src/Pure/Isar/context_rules.ML Wed Jan 21 16:47:32 2009 +0100 +++ b/src/Pure/Isar/context_rules.ML Wed Jan 21 16:48:15 2009 +0100 @@ -199,7 +199,7 @@ val dest_query = rule_add elim_queryK Tactic.make_elim; val _ = Context.>> (Context.map_theory - (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])])); + (snd o PureThy.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])])); (* concrete syntax *)