cleanup

--- a/src/HOL/Integ/NatBin.thy	Wed Feb 14 10:06:14 2007 +0100
+++ b/src/HOL/Integ/NatBin.thy	Wed Feb 14 10:06:15 2007 +0100
@@ -14,10 +14,8 @@
   Arithmetic for naturals is reduced to that for the non-negative integers.
 *}
 
-instance nat :: number ..
-
-defs (overloaded)
-  nat_number_of_def: "number_of v == nat (number_of (v\<Colon>int))"
+instance nat :: number
+  nat_number_of_def: "number_of v == nat (number_of (v\<Colon>int))" ..
 
 abbreviation (xsymbols)
   square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where

--- a/src/HOL/ex/CodeEval.thy	Wed Feb 14 10:06:14 2007 +0100
+++ b/src/HOL/ex/CodeEval.thy	Wed Feb 14 10:06:15 2007 +0100
@@ -154,6 +154,7 @@
 
 subsection {* Small examples *}
 
+ML {* Eval.term "(Suc 2 + 1) * 4" *}
 ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *}
 ML {* Eval.term "[]::nat list" *}
 ML {* Eval.term "fst ([]::nat list, Suc 0) = []" *}

--- a/src/Pure/General/alist.ML	Wed Feb 14 10:06:14 2007 +0100
+++ b/src/Pure/General/alist.ML	Wed Feb 14 10:06:15 2007 +0100
@@ -23,9 +23,9 @@
   val map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)
     -> ('a * 'b) list -> ('a * 'b) list
   val join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)
-    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list      (*exception DUP*)
+    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list    (*exception DUP*)
   val merge: ('a * 'a -> bool) -> ('b * 'b -> bool)
-    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list      (*exception DUP*)
+    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list    (*exception DUP*)
   val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
   val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
   val coalesce: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list

--- a/src/Pure/Tools/codegen_data.ML	Wed Feb 14 10:06:14 2007 +0100
+++ b/src/Pure/Tools/codegen_data.ML	Wed Feb 14 10:06:15 2007 +0100
@@ -658,6 +658,10 @@
        (c, (Susp.value [], [])) (add_thm thm)) funcs)) thy
   end;
 
+fun delete_force msg key xs =
+  if AList.defined (op =) xs key then AList.delete (op =) key xs
+  else error ("No such " ^ msg ^ ": " ^ quote key);
+
 val add_func = gen_add_func true;
 val add_func_legacy = gen_add_func false;
 
@@ -710,13 +714,13 @@
   (map_exec_purge NONE o map_preproc o apfst o apsnd) (AList.update (op =) (name, (serial (), f)));
 
 fun del_inline_proc name =
-  (map_exec_purge NONE o map_preproc o apfst o apsnd) (AList.delete (op =) name);
+  (map_exec_purge NONE o map_preproc o apfst o apsnd) (delete_force "inline procedure" name);
 
 fun add_preproc (name, f) =
   (map_exec_purge NONE o map_preproc o apsnd) (AList.update (op =) (name, (serial (), f)));
 
 fun del_preproc name =
-  (map_exec_purge NONE o map_preproc o apsnd) (AList.delete (op =) name);
+  (map_exec_purge NONE o map_preproc o apsnd) (delete_force "preprocessor" name);
 
 local
 
@@ -763,9 +767,7 @@
     val thy = Thm.theory_of_cterm ct;
   in
     ct
-    |> Thm.reflexive
-    |> fold (rhs_conv o MetaSimplifier.rewrite false o single)
-        ((#inlines o the_preproc o get_exec) thy)
+    |> MetaSimplifier.rewrite false ((#inlines o the_preproc o get_exec) thy)
     |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
         ((#inline_procs o the_preproc o get_exec) thy)
   end;