permissive update for improved "tool compliance";
authorwenzelm
Sun Nov 27 22:20:07 2011 +0100 (2011-11-27)
changeset 4565218214436e1d3
parent 45651 172aa230ce69
child 45653 63ed1be524eb
permissive update for improved "tool compliance";
tuned;
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Sun Nov 27 22:03:22 2011 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sun Nov 27 22:20:07 2011 +0100
     1.3 @@ -187,9 +187,8 @@
     1.4  type inductive_info = {names: string list, coind: bool} * inductive_result;
     1.5  
     1.6  val empty_equations =
     1.7 -  Item_Net.init
     1.8 -    (op aconv o pairself Thm.prop_of)
     1.9 -    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);  (* FIXME fragile wrt. morphisms *)
    1.10 +  Item_Net.init Thm.eq_thm_prop
    1.11 +    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);
    1.12  
    1.13  datatype data = Data of
    1.14   {infos: inductive_info Symtab.table,
    1.15 @@ -273,9 +272,10 @@
    1.16  
    1.17  val get_equations = #equations o rep_data;
    1.18  
    1.19 -val equation_add =
    1.20 +val equation_add_permissive =
    1.21    Thm.declaration_attribute (fn thm =>
    1.22 -    map_data (fn (infos, monos, equations) => (infos, monos, Item_Net.update thm equations)));
    1.23 +    map_data (fn (infos, monos, equations) =>
    1.24 +      (infos, monos, perhaps (try (Item_Net.update thm)) equations)));
    1.25  
    1.26  
    1.27  
    1.28 @@ -885,7 +885,7 @@
    1.29      val (eqs', lthy3) = lthy2 |>
    1.30        fold_map (fn (name, eq) => Local_Theory.note
    1.31            ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"),
    1.32 -            [Attrib.internal (K equation_add)]), [eq])
    1.33 +            [Attrib.internal (K equation_add_permissive)]), [eq])
    1.34            #> apfst (hd o snd))
    1.35          (if null eqs then [] else (cnames ~~ eqs))
    1.36      val (inducts, lthy4) =