more permissive
authorhaftmann
Thu Sep 20 16:37:31 2007 +0200 (2007-09-20)
changeset 246596b7ac2a43df8
parent 24658 49adbdcc52e2
child 24660 8f94b16783f7
more permissive
src/HOL/Library/Eval.thy
src/HOL/ex/Eval_Examples.thy
src/Pure/Isar/code.ML
     1.1 --- a/src/HOL/Library/Eval.thy	Thu Sep 20 16:37:30 2007 +0200
     1.2 +++ b/src/HOL/Library/Eval.thy	Thu Sep 20 16:37:31 2007 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4        |> snd
     1.5      end;
     1.6    fun hook specs =
     1.7 -    if (fst o hd) specs = (fst o dest_Type) @{typ typ} then I
     1.8 +    if null specs orelse (fst o hd) specs = (fst o dest_Type) @{typ typ} then I
     1.9      else
    1.10        DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
    1.11        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
     2.1 --- a/src/HOL/ex/Eval_Examples.thy	Thu Sep 20 16:37:30 2007 +0200
     2.2 +++ b/src/HOL/ex/Eval_Examples.thy	Thu Sep 20 16:37:31 2007 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Small examples for evaluation mechanisms *}
     2.5  
     2.6  theory Eval_Examples
     2.7 -imports Eval
     2.8 +imports Eval "~~/src/HOL/Real/Rational"
     2.9  begin
    2.10  
    2.11  text {* SML evaluation oracle *}
    2.12 @@ -34,6 +34,8 @@
    2.13  value "[]::nat list"
    2.14  value "[(nat 100, ())]"
    2.15  value "max (2::int) 4"
    2.16 +value "of_int 2 / of_int 4 * (1::rat)"
    2.17 +
    2.18  
    2.19  text {* a fancy datatype *}
    2.20  
     3.1 --- a/src/Pure/Isar/code.ML	Thu Sep 20 16:37:30 2007 +0200
     3.2 +++ b/src/Pure/Isar/code.ML	Thu Sep 20 16:37:31 2007 +0200
     3.3 @@ -718,13 +718,13 @@
     3.4      | NONE => thy;
     3.5  
     3.6  fun del_func thm thy =
     3.7 -  let
     3.8 -    val func = mk_func thm;
     3.9 -    val const = const_of_func thy func;
    3.10 -  in map_exec_purge (SOME [const]) (map_funcs
    3.11 -    (Symtab.map_entry
    3.12 -      const (del_thm func))) thy
    3.13 -  end;
    3.14 +  case mk_liberal_func thm
    3.15 +   of SOME func => let
    3.16 +          val c = const_of_func thy func;
    3.17 +        in map_exec_purge (SOME [c]) (map_funcs
    3.18 +          (Symtab.map_entry c (del_thm func))) thy
    3.19 +        end
    3.20 +    | NONE => thy;
    3.21  
    3.22  fun add_funcl (const, lthms) thy =
    3.23    let