# HG changeset patch
# User wenzelm
# Date 1322428807 -3600
# Node ID 18214436e1d39584acffe38d3d05cc53f90ebebc
# Parent  172aa230ce6910d7b45ce20eca017e4de9355cea
permissive update for improved "tool compliance";
tuned;

diff -r 172aa230ce69 -r 18214436e1d3 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Nov 27 22:03:22 2011 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Nov 27 22:20:07 2011 +0100
@@ -187,9 +187,8 @@
 type inductive_info = {names: string list, coind: bool} * inductive_result;
 
 val empty_equations =
-  Item_Net.init
-    (op aconv o pairself Thm.prop_of)
-    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);  (* FIXME fragile wrt. morphisms *)
+  Item_Net.init Thm.eq_thm_prop
+    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);
 
 datatype data = Data of
  {infos: inductive_info Symtab.table,
@@ -273,9 +272,10 @@
 
 val get_equations = #equations o rep_data;
 
-val equation_add =
+val equation_add_permissive =
   Thm.declaration_attribute (fn thm =>
-    map_data (fn (infos, monos, equations) => (infos, monos, Item_Net.update thm equations)));
+    map_data (fn (infos, monos, equations) =>
+      (infos, monos, perhaps (try (Item_Net.update thm)) equations)));
 
 
 
@@ -885,7 +885,7 @@
     val (eqs', lthy3) = lthy2 |>
       fold_map (fn (name, eq) => Local_Theory.note
           ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"),
-            [Attrib.internal (K equation_add)]), [eq])
+            [Attrib.internal (K equation_add_permissive)]), [eq])
           #> apfst (hd o snd))
         (if null eqs then [] else (cnames ~~ eqs))
     val (inducts, lthy4) =