# HG changeset patch
# User haftmann
# Date 1232552895 -3600
# Node ID 0950f4f0d0cd8ccd0f80acf8d85f620796a472a1
# Parent  b3b33e0298ebab6cb84ce8579bd8ec41eea8bdf4
binding replaces bstring

diff -r b3b33e0298eb -r 0950f4f0d0cd src/Pure/Isar/context_rules.ML
--- 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 *)