Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
binding replaces bstring
authorhaftmann
Wed, 21 Jan 2009 16:48:15 +0100
changeset 29582 0950f4f0d0cd
parent 29581 b3b33e0298eb
child 29583 1f930609dcd0
binding replaces bstring
src/Pure/Isar/context_rules.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle