silenced subsumption warnings for default code equations entirely
authorhaftmann
Sun Jul 28 05:32:02 2013 +0200 (2013-07-28)
changeset 52781e78c3023162b
parent 52780 4b6b71fb00d5
child 52783 084ac81e9871
silenced subsumption warnings for default code equations entirely
src/Pure/Isar/code.ML
     1.1 --- a/src/Pure/Isar/code.ML	Mon Jul 29 20:51:05 2013 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Sun Jul 28 05:32:02 2013 +0200
     1.3 @@ -1039,7 +1039,7 @@
     1.4    let
     1.5      val thm = Thm.close_derivation raw_thm;
     1.6      val c = const_eqn thy thm;
     1.7 -    fun update_subsume thy (thm, proper) eqns = 
     1.8 +    fun update_subsume thy verbose (thm, proper) eqns = 
     1.9        let
    1.10          val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
    1.11            o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
    1.12 @@ -1054,17 +1054,17 @@
    1.13            end;
    1.14          fun drop (thm', proper') = if (proper orelse not proper')
    1.15            andalso matches_args (args_of thm') then 
    1.16 -            (warning ("Code generator: dropping subsumed code equation\n" ^
    1.17 -                Display.string_of_thm_global thy thm'); true)
    1.18 +            (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
    1.19 +                Display.string_of_thm_global thy thm') else (); true)
    1.20            else false;
    1.21        in (thm, proper) :: filter_out drop eqns end;
    1.22      fun natural_order thy_ref eqns =
    1.23 -      (eqns, Lazy.lazy (fn () => fold (update_subsume (Theory.deref thy_ref)) eqns []))
    1.24 +      (eqns, Lazy.lazy (fn () => fold (update_subsume (Theory.deref thy_ref) false) eqns []))
    1.25      fun add_eqn' true (Default (eqns, _)) =
    1.26            Default (natural_order (Theory.check_thy thy) ((thm, proper) :: eqns))
    1.27            (*this restores the natural order and drops syntactic redundancies*)
    1.28        | add_eqn' true fun_spec = fun_spec
    1.29 -      | add_eqn' false (Eqns eqns) = Eqns (update_subsume thy (thm, proper) eqns)
    1.30 +      | add_eqn' false (Eqns eqns) = Eqns (update_subsume thy true (thm, proper) eqns)
    1.31        | add_eqn' false _ = Eqns [(thm, proper)];
    1.32    in change_fun_spec false c (add_eqn' default) thy end;
    1.33