# HG changeset patch
# User haftmann
# Date 1190299051 -7200
# Node ID 6b7ac2a43df81c40bee59863c82927599b6272cf
# Parent  49adbdcc52e2ec72cc0d60600d0804815442f22f
more permissive

diff -r 49adbdcc52e2 -r 6b7ac2a43df8 src/HOL/Library/Eval.thy
--- 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)
diff -r 49adbdcc52e2 -r 6b7ac2a43df8 src/HOL/ex/Eval_Examples.thy
--- 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 *}
 
diff -r 49adbdcc52e2 -r 6b7ac2a43df8 src/Pure/Isar/code.ML
--- 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