# HG changeset patch
# User wenzelm
# Date 1377531452 -7200
# Node ID 1d248d75620ea94acf41ee1a11f3c577a9599f7e
# Parent  cf40231bc30517ef48758b0142ad4ab08981a70d# Parent  bec95e287d266defbffbbe4e871875c75edb2a27
merged

diff -r cf40231bc305 -r 1d248d75620e Admin/lib/Tools/build_doc
--- a/Admin/lib/Tools/build_doc	Mon Aug 26 14:14:33 2013 +0200
+++ b/Admin/lib/Tools/build_doc	Mon Aug 26 17:37:32 2013 +0200
@@ -17,6 +17,7 @@
   echo "  Options are:"
   echo "    -a           select all doc sessions"
   echo "    -j INT       maximum number of parallel jobs (default 1)"
+  echo "    -s           system build mode"
   echo
   echo "  Build Isabelle documentation from (doc) sessions."
   echo
@@ -37,12 +38,14 @@
 
 ## process command line
 
+declare -a BUILD_ARGS=()
+
+
 # options
 
 ALL_DOCS="false"
-JOBS=""
 
-while getopts "aj:" OPT
+while getopts "aj:s" OPT
 do
   case "$OPT" in
     a)
@@ -50,7 +53,11 @@
       ;;
     j)
       check_number "$OPTARG"
-      JOBS="-j $OPTARG"
+      BUILD_ARGS["${#BUILD_ARGS[@]}"]="-j"
+      BUILD_ARGS["${#BUILD_ARGS[@]}"]="$OPTARG"
+      ;;
+    s)
+      BUILD_ARGS["${#BUILD_ARGS[@]}"]="-s"
       ;;
     \?)
       usage
@@ -64,9 +71,9 @@
 # arguments
 
 if [ "$ALL_DOCS" = true ]; then
-  declare -a BUILD_ARGS=(-g doc)
+  BUILD_ARGS["${#BUILD_ARGS[@]}"]="-g"
+  BUILD_ARGS["${#BUILD_ARGS[@]}"]="doc"
 else
-  declare -a BUILD_ARGS=()
   [ "$#" -eq 0 ] && usage
 fi
 
@@ -83,12 +90,12 @@
 OUTPUT="$ISABELLE_TMP_PREFIX$$"
 mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\""
 
-"$ISABELLE_TOOL" build -R -b $JOBS "${BUILD_ARGS[@]}"
+"$ISABELLE_TOOL" build -R -b "${BUILD_ARGS[@]}"
 RC=$?
 
 if [ "$RC" = 0 ]; then
   "$ISABELLE_TOOL" build -o browser_info=false -o "document=pdf" \
-    -o "document_output=$OUTPUT" -c $JOBS "${BUILD_ARGS[@]}"
+    -o "document_output=$OUTPUT" -c "${BUILD_ARGS[@]}"
   RC=$?
 fi
 
diff -r cf40231bc305 -r 1d248d75620e Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Mon Aug 26 14:14:33 2013 +0200
+++ b/Admin/lib/Tools/makedist	Mon Aug 26 17:37:32 2013 +0200
@@ -176,11 +176,11 @@
 
 cp -a src src.orig
 env ISABELLE_IDENTIFIER="${DISTNAME}-build" \
-  ./bin/isabelle build_doc $JOBS -a || fail "Failed to build documentation"
+  ./bin/isabelle build_doc $JOBS -s -a || fail "Failed to build documentation"
 rm -rf src
 mv src.orig src
 
-rm -rf Admin
+rm -rf Admin browser_info heaps
 
 
 # create archive
diff -r cf40231bc305 -r 1d248d75620e src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Aug 26 14:14:33 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Aug 26 17:37:32 2013 +0200
@@ -406,7 +406,7 @@
     val absrep_trm =  quot_thm_abs quot_thm
     val rty_forced = (domain_type o fastype_of) absrep_trm
     val forced_rhs = force_rty_type lthy rty_forced rhs
-    val lhs = Free (Binding.print (#1 var), qty)
+    val lhs = Free (Binding.name_of (#1 var), qty)
     val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs)
     val (_, prop') = Local_Defs.cert_def lthy prop
     val (_, newrhs) = Local_Defs.abs_def prop'
@@ -414,7 +414,7 @@
     val ((_, (_ , def_thm)), lthy') = 
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
-    val transfer_rule = generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm
+    val transfer_rule = generate_transfer_rule lthy' quot_thm rsp_thm def_thm opt_par_thm
 
     val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
     val opt_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
diff -r cf40231bc305 -r 1d248d75620e src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Aug 26 14:14:33 2013 +0200
+++ b/src/Pure/more_thm.ML	Mon Aug 26 17:37:32 2013 +0200
@@ -407,7 +407,7 @@
 fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
 
 fun apply_attribute (att: attribute) th x =
-  let val (x', th') = att (x, th)
+  let val (x', th') = att (x, Thm.transfer (Context.theory_of x) th)
   in (the_default th th', the_default x x') end;
 
 fun attribute_declaration att th x = #2 (apply_attribute att th x);