# HG changeset patch
# User chaieb
# Date 1236194552 0
# Node ID 2ec2df1a1665c195a86516eeb6477fdb5d5c0f20
# Parent  7b8afdfa2f8370856bc03651f4f23ffeb642bf09# Parent  2e8a7d86321e8df3d9ac191d1ccc80b8812e9e94
merged

diff -r 2e8a7d86321e -r 2ec2df1a1665 NEWS
--- a/NEWS	Wed Mar 04 19:21:56 2009 +0000
+++ b/NEWS	Wed Mar 04 19:22:32 2009 +0000
@@ -501,7 +501,7 @@
     Suc_not_Zero Zero_not_Suc   ~> nat.distinct
 
 * The option datatype has been moved to a new theory HOL/Option.thy.
-Renamed option_map to Option.map.
+Renamed option_map to Option.map, and o2s to Option.set.
 
 * Library/Nat_Infinity: added addition, numeral syntax and more
 instantiations for algebraic structures.  Removed some duplicate
diff -r 2e8a7d86321e -r 2ec2df1a1665 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Mar 04 19:21:56 2009 +0000
+++ b/src/HOL/HOL.thy	Wed Mar 04 19:22:32 2009 +0000
@@ -1709,6 +1709,11 @@
 subsection {* Nitpick theorem store *}
 
 ML {*
+structure Nitpick_Const_Def_Thms = NamedThmsFun
+(
+  val name = "nitpick_const_def"
+  val description = "alternative definitions of constants as needed by Nitpick"
+)
 structure Nitpick_Const_Simp_Thms = NamedThmsFun
 (
   val name = "nitpick_const_simp"
@@ -1725,7 +1730,8 @@
   val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
 )
 *}
-setup {* Nitpick_Const_Simp_Thms.setup
+setup {* Nitpick_Const_Def_Thms.setup
+         #> Nitpick_Const_Simp_Thms.setup
          #> Nitpick_Const_Psimp_Thms.setup
          #> Nitpick_Ind_Intro_Thms.setup *}
 
diff -r 2e8a7d86321e -r 2ec2df1a1665 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Mar 04 19:21:56 2009 +0000
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Mar 04 19:22:32 2009 +0000
@@ -374,7 +374,9 @@
          in
            lthy''
            |> LocalTheory.note Thm.theoremK ((qualify (Binding.name "simps"),
-             [Attrib.internal (K Simplifier.simp_add)]), maps snd simps')
+                map (Attrib.internal o K)
+                    [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
+                maps snd simps')
            |> snd
          end)
       [goals] |>
diff -r 2e8a7d86321e -r 2ec2df1a1665 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Mar 04 19:21:56 2009 +0000
+++ b/src/HOL/Statespace/state_space.ML	Wed Mar 04 19:22:32 2009 +0000
@@ -611,7 +611,7 @@
            Syntax.const "StateFun.lookup"$Syntax.free (project_name T)$Syntax.free n$s
        | NONE =>
            if get_silent (Context.Proof ctxt)
-	   then Syntax.const "StateFun.lookup"$Syntax.const "arbitrary"$Syntax.free n$s
+	   then Syntax.const "StateFun.lookup" $ Syntax.const "undefined" $ Syntax.free n $ s
            else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[]));
 
 fun lookup_tr ctxt [s,Free (n,_)] = gen_lookup_tr ctxt s n;
@@ -637,8 +637,8 @@
       | NONE =>
          if get_silent (Context.Proof ctxt)
          then Syntax.const "StateFun.update"$
-                   Syntax.const "arbitrary"$Syntax.const "arbitrary"$
-                   Syntax.free n$(Syntax.const KN $ v)$s
+                   Syntax.const "undefined" $ Syntax.const "undefined" $
+                   Syntax.free n $ (Syntax.const KN $ v) $ s
          else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined",[]))
    end;
 
diff -r 2e8a7d86321e -r 2ec2df1a1665 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Mar 04 19:21:56 2009 +0000
+++ b/src/HOL/Tools/datatype_package.ML	Wed Mar 04 19:22:32 2009 +0000
@@ -629,14 +629,6 @@
 
 (** a datatype antiquotation **)
 
-local
-
-val sym_datatype = Pretty.command "datatype";
-val sym_binder = Pretty.str "\\ {\\isacharequal}"; (*FIXME use proper symbol*)
-val sym_sep = Pretty.str "{\\isacharbar}\\ ";
-
-in
-
 fun args_datatype (ctxt, args) =
   let
     val (tyco, (ctxt', args')) = Args.tyname (ctxt, args);
@@ -654,26 +646,19 @@
       in if member (op =) s " " then Pretty.enclose "(" ")" [p]
         else p
       end;
-    fun pretty_constr (co, []) =
-          Syntax.pretty_term ctxt (Const (co, ty))
-      | pretty_constr (co, [ty']) =
-          (Pretty.block o Pretty.breaks)
-            [Syntax.pretty_term ctxt (Const (co, ty' --> ty)),
-              pretty_typ_br ty']
-      | pretty_constr (co, tys) =
-          (Pretty.block o Pretty.breaks)
-            (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
-              map pretty_typ_br tys);
+    fun pretty_constr (co, tys) =
+      (Pretty.block o Pretty.breaks)
+        (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
+          map pretty_typ_br tys);
   in
     Pretty.block
-      (sym_datatype :: Pretty.brk 1 ::
+      (Pretty.command "datatype" :: Pretty.brk 1 ::
        Syntax.pretty_typ ctxt ty ::
-       sym_binder :: Pretty.brk 1 ::
-       flat (separate [Pretty.brk 1, sym_sep]
+       Pretty.str " =" :: Pretty.brk 1 ::
+       flat (separate [Pretty.brk 1, Pretty.str "| "]
          (map (single o pretty_constr) cos)))
   end
 
-end;
 
 (** package setup **)