permissive code attribute; all_eqns

--- a/src/Pure/Isar/code.ML	Mon Jun 15 16:13:03 2009 +0200
+++ b/src/Pure/Isar/code.ML	Mon Jun 15 16:13:04 2009 +0200
@@ -30,6 +30,7 @@
 
   (*code equations*)
   val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
+  val mk_eqn_warning: theory -> (string -> bool) -> thm -> (thm * bool) option
   val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option
   val assert_eqn: theory -> thm * bool -> thm * bool
   val assert_eqns_const: theory -> string
@@ -72,6 +73,7 @@
   val get_datatype_of_constr: theory -> string -> string option
   val default_typscheme: theory -> string -> (string * sort) list * typ
   val these_eqns: theory -> string -> (thm * bool) list
+  val all_eqns: theory -> (thm * bool) list
   val get_case_scheme: theory -> string -> (int * (int * string list)) option
   val is_undefined: theory -> string -> bool
   val print_codesetup: theory -> unit
@@ -363,6 +365,7 @@
 exception BAD_THM of string;
 fun bad_thm msg = raise BAD_THM msg;
 fun error_thm f thm = f thm handle BAD_THM msg => error msg;
+fun warning_thm f thm = SOME (f thm) handle BAD_THM msg => (warning msg; NONE)
 fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
 
 fun is_linear thm =
@@ -445,6 +448,10 @@
 fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o
   apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy));
 
+fun mk_eqn_warning thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm))
+  o warning_thm (gen_assert_eqn thy is_constr_head (K true))
+  o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
+
 fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm))
   o try_thm (gen_assert_eqn thy is_constr_head (K true))
   o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
@@ -861,6 +868,11 @@
 fun add_eqn thm thy =
   gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, true)) thy;
 
+fun add_warning_eqn thm thy =
+  case mk_eqn_warning thy (is_constr thy) thm
+   of SOME eqn => gen_add_eqn false eqn thy
+    | NONE => thy;
+
 fun add_default_eqn thm thy =
   case mk_eqn_liberal thy (is_constr thy) thm
    of SOME eqn => gen_add_eqn true eqn thy
@@ -938,7 +950,7 @@
         || Scan.succeed (mk_attribute add))
   in
     TypeInterpretation.init
-    #> add_del_attribute ("", (add_eqn, del_eqn))
+    #> add_del_attribute ("", (add_warning_eqn, del_eqn))
     #> add_simple_attribute ("nbe", add_nbe_eqn)
   end));
 
@@ -947,6 +959,10 @@
   |> (map o apfst) (Thm.transfer thy)
   |> burrow_fst (common_typ_eqns thy);
 
+fun all_eqns thy =
+  Symtab.dest ((the_eqns o the_exec) thy)
+  |> maps (Lazy.force o snd o snd o fst o snd);
+
 fun default_typscheme thy c =
   let
     fun the_const_typscheme c = (curry (typscheme thy) c o snd o dest_Const