# HG changeset patch
# User haftmann
# Date 1174402357 -3600
# Node ID b20bc8029edb5f13d2b50ea1d6e1d0e3ab37fba1
# Parent  de15ea8fb348bdadf99971f0ac32d630079f3ff0
switched exception from arbitrary to undefined

diff -r de15ea8fb348 -r b20bc8029edb src/HOL/Code_Generator.thy
--- 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
diff -r de15ea8fb348 -r b20bc8029edb src/HOL/Tools/datatype_codegen.ML
--- 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;
 
 
diff -r de15ea8fb348 -r b20bc8029edb src/HOL/Tools/datatype_package.ML
--- 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 $
diff -r de15ea8fb348 -r b20bc8029edb src/HOL/Tools/primrec_package.ML
--- 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)