--- a/src/HOL/Code_Generator.thy Tue Mar 20 10:23:31 2007 +0100
+++ b/src/HOL/Code_Generator.thy Tue Mar 20 15:52:37 2007 +0100
@@ -172,15 +172,12 @@
by rule+
-text {* code generation for arbitrary as exception *}
+text {* code generation for undefined as exception *}
-setup {*
- CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
- #> CodegenSerializer.add_undefined "OCaml" "arbitrary" "(failwith \"arbitrary\")"
-*}
-
-code_const arbitrary
- (Haskell "error/ \"arbitrary\"")
+code_const undefined
+ (SML "(raise Fail \"undefined\")")
+ (OCaml "(failwith \"undefined\")")
+ (Haskell "error/ \"undefined\"")
code_reserved SML Fail
code_reserved OCaml failwith
--- a/src/HOL/Tools/datatype_codegen.ML Tue Mar 20 10:23:31 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Tue Mar 20 15:52:37 2007 +0100
@@ -340,7 +340,7 @@
val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
in case t'
- of Const ("undefined", _) => NONE
+ of Const ("HOL.undefined", _) => NONE
| _ => SOME (c', t')
end;
in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts' |> map_filter I)) end;
@@ -423,7 +423,7 @@
let
val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
in
- fold_rev CodegenData.add_func case_rewrites thy
+ fold_rev (CodegenData.add_func true) case_rewrites thy
end;
--- a/src/HOL/Tools/datatype_package.ML Tue Mar 20 10:23:31 2007 +0100
+++ b/src/HOL/Tools/datatype_package.ML Tue Mar 20 15:52:37 2007 +0100
@@ -433,7 +433,7 @@
(DatatypeProp.make_tnames (map (typ_of_dtyp descr sorts) dt)),
case default of
NONE => (warning ("No clause for constructor " ^ s ^
- " in case expression"); Const ("undefined", dummyT))
+ " in case expression"); Const ("HOL.undefined", dummyT))
| SOME t => t), cases)
| SOME (c as ((_, vs), t)) =>
if length dt <> length vs then
@@ -486,7 +486,7 @@
(fold_rev count_cases cases []);
fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
list_comb (Syntax.const cname, vs) $ body;
- fun is_undefined (Const ("undefined", _)) = true
+ fun is_undefined (Const ("HOL.undefined", _)) = true
| is_undefined _ = false;
in
Syntax.const "_case_syntax" $ x $
--- a/src/HOL/Tools/primrec_package.ML Tue Mar 20 10:23:31 2007 +0100
+++ b/src/HOL/Tools/primrec_package.ML Tue Mar 20 15:52:37 2007 +0100
@@ -142,7 +142,7 @@
(case AList.lookup (op =) eqns cname of
NONE => (warning ("No equation for constructor " ^ quote cname ^
"\nin definition of function " ^ quote fname);
- (fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
+ (fnameTs', fnss', (Const ("HOL.undefined", dummyT))::fns))
| SOME (ls, cargs', rs, rhs, eq) =>
let
val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
@@ -182,7 +182,7 @@
case AList.lookup (op =) fns i of
NONE =>
let
- val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
+ val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
dummyT ---> HOLogic.unitT)) constrs;
val _ = warning ("No function definition for datatype " ^ quote tname)