merged

--- a/Admin/makebin	Fri Apr 03 16:17:50 2009 +0200
+++ b/Admin/makebin	Fri Apr 03 16:18:14 2009 +0200
@@ -1,17 +1,12 @@
 #!/usr/bin/env bash
 #
-# $Id$
-#
-# makebin -- make Isabelle logic images for current platform.
+# makebin -- make Isabelle logic images for current platform
 
 
 ## global settings
 
 TMP="/var/tmp/isabelle-makebin$$"
 
-TAR=tar
-type -path gtar >/dev/null && TAR=gtar
-
 export THIS_IS_ISABELLE_MAKEBIN=true
 
 
@@ -75,11 +70,11 @@
 ## main
 
 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
-ARCHIVE_BASE=$(basename "$ARCHIVE")
-ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
+ARCHIVE_BASE="$(basename "$ARCHIVE")"
+ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
 
-ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
+ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
 ISABELLE_HOME="$TMP/$ISABELLE_NAME"
 
 
@@ -88,16 +83,16 @@
 mkdir "$TMP" || fail "Cannot create directory $TMP"
 
 cd "$TMP"
-"$TAR" xzf "$ARCHIVE_FULL"
+tar xzf "$ARCHIVE_FULL"
 cd "$ISABELLE_NAME"
 
 perl -pi \
-  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \
-  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \
+  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \
+  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-M 1 -p 2":;' \
   etc/settings
 
 if [ -n "$DO_LIBRARY" ]; then
-  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1 -i true -d pdf -V outline=/proof,/ML":;' \
+  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -i true -d pdf -V outline=/proof,/ML":;' \
     etc/settings
 fi
 
@@ -134,13 +129,13 @@
 chgrp -R isabelle "$TMP"
 
 if [ -n "$DO_LIBRARY" ]; then
-  "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
+  tar cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
     gzip -f "${ISABELLE_NAME}_library.tar"
     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
 else
   for IMG in HOL HOL-Nominal ZF
   do
-    "$TAR" cf "${IMG}_$PLATFORM.tar" \
+    tar cf "${IMG}_$PLATFORM.tar" \
       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
     gzip -f "${IMG}_$PLATFORM.tar"

--- a/src/HOL/Tools/inductive_set_package.ML	Fri Apr 03 16:17:50 2009 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Fri Apr 03 16:18:14 2009 +0200
@@ -435,12 +435,19 @@
        | NONE => (x, (x, (x, x))))) params;
     val (params1, (params2, params3)) =
       params' |> map snd |> split_list ||> split_list;
+    val paramTs = map fastype_of params;
 
     (* equations for converting sets to predicates *)
     val ((cs', cs_info), eqns) = cs |> map (fn c as Free (s, T) =>
       let
         val fs = the_default [] (AList.lookup op = new_arities c);
-        val (_, U) = split_last (binder_types T);
+        val (Us, U) = split_last (binder_types T);
+        val _ = Us = paramTs orelse error (Pretty.string_of (Pretty.chunks
+          [Pretty.str "Argument types",
+           Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) Us)),
+           Pretty.str ("of " ^ s ^ " do not agree with types"),
+           Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
+           Pretty.str "of declared parameters"]));
         val Ts = HOLogic.prodT_factors' fs U;
         val c' = Free (s ^ "p",
           map fastype_of params1 @ Ts ---> HOLogic.boolT)