--- a/src/HOL/Library/Eval.thy Thu Sep 20 16:37:30 2007 +0200
+++ b/src/HOL/Library/Eval.thy Thu Sep 20 16:37:31 2007 +0200
@@ -113,7 +113,7 @@
|> snd
end;
fun hook specs =
- if (fst o hd) specs = (fst o dest_Type) @{typ typ} then I
+ if null specs orelse (fst o hd) specs = (fst o dest_Type) @{typ typ} then I
else
DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
(map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
--- a/src/HOL/ex/Eval_Examples.thy Thu Sep 20 16:37:30 2007 +0200
+++ b/src/HOL/ex/Eval_Examples.thy Thu Sep 20 16:37:31 2007 +0200
@@ -5,7 +5,7 @@
header {* Small examples for evaluation mechanisms *}
theory Eval_Examples
-imports Eval
+imports Eval "~~/src/HOL/Real/Rational"
begin
text {* SML evaluation oracle *}
@@ -34,6 +34,8 @@
value "[]::nat list"
value "[(nat 100, ())]"
value "max (2::int) 4"
+value "of_int 2 / of_int 4 * (1::rat)"
+
text {* a fancy datatype *}
--- a/src/Pure/Isar/code.ML Thu Sep 20 16:37:30 2007 +0200
+++ b/src/Pure/Isar/code.ML Thu Sep 20 16:37:31 2007 +0200
@@ -718,13 +718,13 @@
| NONE => thy;
fun del_func thm thy =
- let
- val func = mk_func thm;
- val const = const_of_func thy func;
- in map_exec_purge (SOME [const]) (map_funcs
- (Symtab.map_entry
- const (del_thm func))) thy
- end;
+ case mk_liberal_func thm
+ of SOME func => let
+ val c = const_of_func thy func;
+ in map_exec_purge (SOME [c]) (map_funcs
+ (Symtab.map_entry c (del_thm func))) thy
+ end
+ | NONE => thy;
fun add_funcl (const, lthms) thy =
let