# HG changeset patch
# User huffman
# Date 1325099152 -3600
# Node ID b4dcefaa17211c53c5d373cd4561c7acafe1e049
# Parent  fad87bb608fcceb81a77fb42045c599738d26eba# Parent  493d9c4d7ed5b612db70aea6cc633f4ef55e0b5c
merged

diff -r fad87bb608fc -r b4dcefaa1721 Admin/PLATFORMS
--- a/Admin/PLATFORMS	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/PLATFORMS	Wed Dec 28 20:05:52 2011 +0100
@@ -61,21 +61,25 @@
 32 bit vs. 64 bit platforms
 ---------------------------
 
-64 bit hardware becomes more and more important for many users.
-Add-on tools need to work seamlessly without manual user
-configuration, although it is often sufficient to fall back on 32 bit
-executables.
+Most users already have 64 bit hardware, and many of them are running
+a 64 bit operating system.  Native 64 bit support for ML and Scala/JVM
+is increasingly important for big Isabelle applications, but 32 bit is
+often the default to get started.  Add-on executables need to work
+seamlessly without manual user configuration, either as native 64 bit
+executables or in 32 bit mode on a 64 bit platform.
 
 The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
-the platform, even on 64 bit hardware.  Power-tools need to indicate
-64 bit support explicitly, via the (optional) ISABELLE_PLATFORM64
-setting.  The following bash expression prefers the 64 bit platform,
-if that is available:
+the platform, even on 64 bit hardware.  Tools need to indicate 64 bit
+support explicitly via the (optional) ISABELLE_PLATFORM64 setting, if
+this is really required.  The following bash expression prefers the 64
+bit platform, if that is available:
 
   "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
 
 Note that ML and JVM may have a different idea of the platform,
-depending on the respective binaries that are actually run.
+depending on the respective binaries that are actually run.  The
+"uname" Unix tool usually only tells about its own executable format,
+not the underlying platform.
 
 
 Dependable system tools
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/isatest-makeall	Wed Dec 28 20:05:52 2011 +0100
@@ -71,12 +71,6 @@
   
     macbroy2)
         MFLAGS="-k"
-        TARGETS=full
-        NICE=""
-        ;;
-
-    macbroy5)
-        MFLAGS="-k -j 2"
         NICE=""
         ;;
 
@@ -102,7 +96,6 @@
 
     macbroy30)
         MFLAGS="-k"
-        TARGETS=full
         NICE=""
         ;;
 
@@ -124,8 +117,13 @@
   TARGETS="$2"
   shift 2
   ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
-  DIR="$ISABELLE_HOME/src/$LOGIC"
-  TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
+  if [ "$LOGIC" = "." ]; then
+    DIR="."
+    TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
+  else
+    DIR="$ISABELLE_HOME/src/$LOGIC"
+    TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
+  fi
 else
   DIR="."
   TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/isatest-makedist	Wed Dec 28 20:05:52 2011 +0100
@@ -107,9 +107,11 @@
 sleep 15
 $SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
 sleep 15
-$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8; $MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8"
-sleep 15
-$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
+$SSH macbroy2 "
+  $MAKEALL $HOME/settings/mac-poly64-M4 -l . full;
+  $MAKEALL $HOME/settings/mac-poly64-M8 -l . full;
+  $MAKEALL $HOME/settings/mac-poly-M4;
+  $MAKEALL $HOME/settings/mac-poly-M8"
 sleep 15
 $SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2"
 sleep 15
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/afp-poly
--- a/Admin/isatest/settings/afp-poly	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/afp-poly	Wed Dec 28 20:05:52 2011 +0100
@@ -28,4 +28,4 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
 
-init_component "$CONTRIB/kodkodi"
+#init_component "$CONTRIB/kodkodi-1.2.16"
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/at-poly
--- a/Admin/isatest/settings/at-poly	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/at-poly	Wed Dec 28 20:05:52 2011 +0100
@@ -24,5 +24,5 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
 
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
 
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/at-poly-e
--- a/Admin/isatest/settings/at-poly-e	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/at-poly-e	Wed Dec 28 20:05:52 2011 +0100
@@ -24,4 +24,4 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
 
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/at-poly-test
--- a/Admin/isatest/settings/at-poly-test	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/at-poly-test	Wed Dec 28 20:05:52 2011 +0100
@@ -28,4 +28,4 @@
 ISABELLE_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml"
 ISABELLE_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl"
 
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/at64-poly
--- a/Admin/isatest/settings/at64-poly	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/at64-poly	Wed Dec 28 20:05:52 2011 +0100
@@ -24,4 +24,4 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
 
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/cygwin-poly-e
--- a/Admin/isatest/settings/cygwin-poly-e	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/cygwin-poly-e	Wed Dec 28 20:05:52 2011 +0100
@@ -24,4 +24,4 @@
 
 ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false"
 
-init_component "$HOME/contrib/kodkodi"
+#init_component "$HOME/contrib/kodkodi-1.2.16"
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly
--- a/Admin/isatest/settings/mac-poly	Wed Dec 28 20:05:28 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-  POLYML_HOME="/home/polyml/polyml-5.2.1"
-  ML_SYSTEM="polyml-5.2.1"
-  ML_PLATFORM="ppc-darwin"
-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 500"
-
-ISABELLE_HOME_USER=~/isabelle-mac-poly
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -g false"
-
-init_component "$HOME/contrib_devel/kodkodi"
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly-M2
--- a/Admin/isatest/settings/mac-poly-M2	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly-M2	Wed Dec 28 20:05:52 2011 +0100
@@ -25,5 +25,5 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 2 -q 2"
 
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
 
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly-M4
--- a/Admin/isatest/settings/mac-poly-M4	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly-M4	Wed Dec 28 20:05:52 2011 +0100
@@ -25,4 +25,4 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
 
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly-M8
--- a/Admin/isatest/settings/mac-poly-M8	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly-M8	Wed Dec 28 20:05:52 2011 +0100
@@ -25,5 +25,5 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
 
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
 
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly64-M2
--- a/Admin/isatest/settings/mac-poly64-M2	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly64-M2	Wed Dec 28 20:05:52 2011 +0100
@@ -25,5 +25,5 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 2 -q 2"
 
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
 
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly64-M4
--- a/Admin/isatest/settings/mac-poly64-M4	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly64-M4	Wed Dec 28 20:05:52 2011 +0100
@@ -25,4 +25,4 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
 
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
diff -r fad87bb608fc -r b4dcefaa1721 Admin/isatest/settings/mac-poly64-M8
--- a/Admin/isatest/settings/mac-poly64-M8	Wed Dec 28 20:05:28 2011 +0100
+++ b/Admin/isatest/settings/mac-poly64-M8	Wed Dec 28 20:05:52 2011 +0100
@@ -25,5 +25,5 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
 
-init_component "$HOME/contrib_devel/kodkodi"
+#init_component "$HOME/contrib_devel/kodkodi-1.2.16"
 
diff -r fad87bb608fc -r b4dcefaa1721 src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Wed Dec 28 20:05:28 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Wed Dec 28 20:05:52 2011 +0100
@@ -12,6 +12,7 @@
   val make_case :  Proof.context -> config -> string list -> term -> (term * term) list -> term
   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
   val case_tr: bool -> Proof.context -> term list -> term
+  val show_cases: bool Config.T
   val case_tr': string -> Proof.context -> term list -> term
   val add_case_tr' : string list -> theory -> theory
   val setup: theory -> theory
@@ -414,27 +415,31 @@
 
 (* print translation *)
 
+val show_cases = Attrib.setup_config_bool @{binding show_cases} (K true);
+
 fun case_tr' cname ctxt ts =
-  let
-    fun mk_clause (pat, rhs) =
-      let val xs = Term.add_frees pat [] in
-        Syntax.const @{syntax_const "_case1"} $
-          map_aterms
-            (fn Free p => Syntax_Trans.mark_boundT p
-              | Const (s, _) => Syntax.const (Lexicon.mark_const s)
-              | t => t) pat $
-          map_aterms
-            (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
-              | t => t) rhs
-      end;
-  in
-    (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of
-      SOME (x, clauses) =>
-        Syntax.const @{syntax_const "_case_syntax"} $ x $
-          foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
-            (map mk_clause clauses)
-    | NONE => raise Match)
-  end;
+  if Config.get ctxt show_cases then
+    let
+      fun mk_clause (pat, rhs) =
+        let val xs = Term.add_frees pat [] in
+          Syntax.const @{syntax_const "_case1"} $
+            map_aterms
+              (fn Free p => Syntax_Trans.mark_boundT p
+                | Const (s, _) => Syntax.const (Lexicon.mark_const s)
+                | t => t) pat $
+            map_aterms
+              (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
+                | t => t) rhs
+        end;
+    in
+      (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of
+        SOME (x, clauses) =>
+          Syntax.const @{syntax_const "_case_syntax"} $ x $
+            foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
+              (map mk_clause clauses)
+      | NONE => raise Match)
+    end
+  else raise Match;
 
 fun add_case_tr' case_names thy =
   Sign.add_advanced_trfuns ([], [],