src/HOL/Tools/inductive_set.ML
changeset 33670 02b7738aef6a
parent 33669 ae9a2ea9a989
child 33671 4b0f2599ed48
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Nov 13 19:57:46 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 13 20:41:29 2009 +0100
     1.3 @@ -505,7 +505,7 @@
     1.4              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
     1.5                [def, mem_Collect_eq, split_conv]) 1))
     1.6          in
     1.7 -          lthy |> LocalTheory.note "" ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
     1.8 +          lthy |> LocalTheory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
     1.9              [Attrib.internal (K pred_set_conv_att)]),
    1.10                [conv_thm]) |> snd
    1.11          end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;