# HG changeset patch # User berghofe # Date 1161252507 -7200 # Node ID e053811d680edffa3b9e684d0ea59723f4099525 # Parent 6048c085c3ae2a133e66406b2e42b9e148d9c698 Induction rule for graph of recursion combinator is now hidden to prevent name collisions with induction rule for nominal datatype. diff -r 6048c085c3ae -r e053811d680e src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Thu Oct 19 11:21:01 2006 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Thu Oct 19 12:08:27 2006 +0200 @@ -1436,13 +1436,16 @@ (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets'); val (thy11, {intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}) = + thy10 |> setmp InductivePackage.quiet_mode (!quiet_mode) (TheoryTarget.init NONE #> InductivePackage.add_inductive_i false big_rec_name false false false (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map (apsnd SOME o dest_Free) rec_fns) (map (fn x => (("", []), x)) rec_intr_ts) [] #> - apfst (snd o LocalTheory.exit false)) thy10; + apfst (snd o LocalTheory.exit false)) |>> + PureThy.hide_thms true [NameSpace.append + (Sign.full_name thy10 big_rec_name) "induct"]; (** equivariance **)