# HG changeset patch
# User wenzelm
# Date 1275665265 -7200
# Node ID 00bfa4276d9cf470236d208bdf50817cde068155
# Parent  81f058f2d2ff46f36e98527be70642b6c0821922# Parent  af2adf0ae97df73350a95c64259245c89531400f
merged

diff -r 81f058f2d2ff -r 00bfa4276d9c Admin/makebundle
--- a/Admin/makebundle	Fri Jun 04 16:55:25 2010 +0200
+++ b/Admin/makebundle	Fri Jun 04 17:27:45 2010 +0200
@@ -2,11 +2,6 @@
 #
 # makebundle -- re-package with add-on components
 
-## global settings
-
-TMP="/var/tmp/isabelle-makebundle$$"
-
-
 ## diagnostics
 
 PRG=$(basename "$0")
@@ -14,9 +9,10 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG ARCHIVE COMPONENTS"
+  echo "Usage: $PRG ARCHIVE PLATFORM"
   echo
-  echo "  Re-package Isabelle distribution with add-on components."
+  echo "  Re-package Isabelle source distribution with add-on components"
+  echo "  and logic images"
   echo
   exit 1
 }
@@ -28,34 +24,37 @@
 }
 
 
-## process command line
+## implicit and explicit arguments
 
-[ "$#" -lt 1 ] && usage
+TMP="/var/tmp/isabelle-makebundle$$"
+mkdir "$TMP" || fail "Cannot create directory $TMP"
+
+LOGICS="HOL HOL-Nominal HOLCF ZF"
+
+[ "$#" -ne 2 ] && usage
 
 ARCHIVE="$1"; shift
+PLATFORM="$1"; shift
 
-declare -a COMPONENTS
-COMPONENTS=("$@")
+[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
 
 
 ## main
 
-mkdir "$TMP" || fail "Cannot create directory $TMP"
-
 ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
 ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
 ISABELLE_HOME="$TMP/$ISABELLE_NAME"
 
-[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
 tar -C "$TMP" -x -z -f "$ARCHIVE"
 
+
 echo "#bundled components" >> "$ISABELLE_HOME/etc/components"
 
-for COMPONENT in "${COMPONENTS[@]}"
+for CONTRIB in "$ARCHIVE_DIR"/contrib/*.tar.gz
 do
-  tar -C "$ISABELLE_HOME/contrib" -x -z -f "$COMPONENT"
-  NAME="$(basename "$COMPONENT" .tar.gz)"
-  [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $COMPONENT"
+  tar -C "$ISABELLE_HOME/contrib" -x -z -f "$CONTRIB"
+  NAME="$(basename "$CONTRIB" .tar.gz)"
+  [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $CONTRIB"
 
   if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then
     echo "component $NAME"
@@ -65,9 +64,20 @@
   fi
 done
 
-tar -C "$TMP" -c -z \
-  -f "${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle.tar.gz" \
-  Isabelle "$ISABELLE_NAME"
+
+for LOGIC in $LOGICS
+do
+  LOGIC_ARCHIVE="$ARCHIVE_DIR/${LOGIC}_${PLATFORM}.tar.gz"
+  [ -f "$LOGIC_ARCHIVE" ] || fail "Bad logic archive: $LOGIC_ARCHIVE"
+  echo "logic $LOGIC"
+  tar -C "$ISABELLE_HOME" -x -z -f "$LOGIC_ARCHIVE"
+done
+
+
+BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"
+
+echo "$(basename "$BUNDLE_ARCHIVE")"
+tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" Isabelle "$ISABELLE_NAME"
 
 
 # clean up
diff -r 81f058f2d2ff -r 00bfa4276d9c src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Jun 04 16:55:25 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Jun 04 17:27:45 2010 +0200
@@ -732,18 +732,20 @@
       prep_decl raw_import I raw_body (ProofContext.init_global thy);
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
 
+    val extraTs =
+      subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
+    val _ =
+      if null extraTs then ()
+      else warning ("Additional type variable(s) in locale specification " ^
+        quote (Binding.str_of binding) ^ ": " ^
+          commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_wrt #1 extraTs)));
+
     val predicate_binding =
       if Binding.is_empty raw_predicate_binding then binding
       else raw_predicate_binding;
     val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
       define_preds predicate_binding parms text thy;
 
-    val extraTs = subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
-    val _ =
-      if null extraTs then ()
-      else warning ("Additional type variable(s) in locale specification " ^
-        quote (Binding.str_of binding));
-
     val a_satisfy = Element.satisfy_morphism a_axioms;
     val b_satisfy = Element.satisfy_morphism b_axioms;
 
diff -r 81f058f2d2ff -r 00bfa4276d9c src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Fri Jun 04 16:55:25 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Fri Jun 04 17:27:45 2010 +0200
@@ -180,13 +180,35 @@
   end;
 
 
-(* consts *)
+(* mixfix notation *)
+
+local
 
 fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
   if not is_locale then (NoSyn, NoSyn, mx)
   else if not is_class then (NoSyn, mx, NoSyn)
   else (mx, NoSyn, NoSyn);
 
+in
+
+fun prep_mixfix ctxt ta (b, extra_tfrees) mx =
+  let
+    val mx' =
+      if null extra_tfrees then mx
+      else
+        (warning
+          ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
+            commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
+            (if mx = NoSyn then ""
+             else "\nDropping mixfix syntax " ^ Pretty.string_of (Syntax.pretty_mixfix mx)));
+          NoSyn);
+  in fork_mixfix ta mx' end;
+
+end;
+
+
+(* consts *)
+
 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
   let
     val b' = Morphism.binding phi b;
@@ -218,10 +240,14 @@
     val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
     val target_ctxt = Local_Theory.target_of lthy;
 
-    val (mx1, mx2, mx3) = fork_mixfix ta mx;
     val t' = Assumption.export_term lthy target_ctxt t;
     val xs = map Free (rev (Variable.add_fixed target_ctxt t' []));
     val u = fold_rev lambda xs t';
+
+    val extra_tfrees =
+      subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+    val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
+
     val global_rhs =
       singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
   in
@@ -261,7 +287,7 @@
     val params = type_params @ term_params;
 
     val U = map Term.fastype_of params ---> T;
-    val (mx1, mx2, mx3) = fork_mixfix ta mx;
+    val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx;
     val (const, lthy') = lthy |>
       (case Class_Target.instantiation_param lthy b of
         SOME c' =>
@@ -299,10 +325,7 @@
     val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
     val T = Term.fastype_of rhs;
     val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
-    val extra_tfrees =
-      fold_types (fold_atyps
-        (fn TFree v => if member (op =) tfreesT v then I else insert (op =) v | _ => I)) rhs []
-      |> sort_wrt #1;
+    val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
 
     (*const*)
     val ((lhs, local_def), lthy2) = lthy |> declare_const ta extra_tfrees xs ((b, T), mx);