Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_set.ML
changeset 33670 02b7738aef6a
parent 33669 ae9a2ea9a989
child 33671 4b0f2599ed48 
--- a/src/HOL/Tools/inductive_set.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 13 20:41:29 2009 +0100
@@ -505,7 +505,7 @@
             (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
               [def, mem_Collect_eq, split_conv]) 1))
         in
-          lthy |> LocalTheory.note "" ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
+          lthy |> LocalTheory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
             [Attrib.internal (K pred_set_conv_att)]),
               [conv_thm]) |> snd
         end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
isabelle