binding replaces bstring
authorhaftmann
Wed Jan 21 16:48:15 2009 +0100 (2009-01-21 ago)
changeset 295820950f4f0d0cd
parent 29581 b3b33e0298eb
child 29583 1f930609dcd0
binding replaces bstring
src/Pure/Isar/context_rules.ML
     1.1 --- a/src/Pure/Isar/context_rules.ML	Wed Jan 21 16:47:32 2009 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Jan 21 16:48:15 2009 +0100
     1.3 @@ -199,7 +199,7 @@
     1.4  val dest_query  = rule_add elim_queryK Tactic.make_elim;
     1.5  
     1.6  val _ = Context.>> (Context.map_theory
     1.7 -  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]));
     1.8 +  (snd o PureThy.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]));
     1.9  
    1.10  
    1.11  (* concrete syntax *)