--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Jan 21 16:51:45 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Jan 21 18:27:43 2009 +0100
@@ -458,12 +458,12 @@
[ind_case_names, RuleCases.consumes 1]);
val ([strong_induct'], thy') = thy |>
Sign.add_path rec_name |>
- PureThy.add_thms [(("strong_induct", #1 strong_induct), #2 strong_induct)];
+ PureThy.add_thms [((Binding.name "strong_induct", #1 strong_induct), #2 strong_induct)];
val strong_inducts =
ProjectRule.projects ctxt (1 upto length names) strong_induct'
in
thy' |>
- PureThy.add_thmss [(("strong_inducts", strong_inducts),
+ PureThy.add_thmss [((Binding.name "strong_inducts", strong_inducts),
[ind_case_names, RuleCases.consumes 1])] |> snd |>
Sign.parent_path
end))