merge
authorblanchet
Tue, 20 Apr 2010 14:39:42 +0200
changeset 36234 77abfa526524
parent 36233 1263bef003b3 (current diff)
parent 36213 4df49260bd82 (diff)
child 36235 61159615a0c5
merge
--- a/Admin/PLATFORMS	Mon Apr 19 19:41:30 2010 +0200
+++ b/Admin/PLATFORMS	Tue Apr 20 14:39:42 2010 +0200
@@ -1,5 +1,5 @@
-Some notes on platform support of Isabelle
-==========================================
+Some notes on multi-platform support of Isabelle
+================================================
 
 Preamble
 --------
@@ -11,32 +11,34 @@
 The basic Isabelle system infrastructure provides some facilities to
 make this work, e.g. see the ML structures File and Path, or functions
 like bash_output.  The settings environment also provides some means
-for portability, e.g. jvm_path to hold up the impression that even
-Java on Windows/Cygwin adheres to Isabelle/POSIX standards.
+for portability, e.g. jvm_path to hold up the impression that Java on
+Windows/Cygwin adheres to Isabelle/POSIX standards.
 
 When producing add-on tools, it is important to stay within this clean
 room of Isabelle, and refrain from overly ambitious system hacking.
+The existing Isabelle scripts follow a certain style that might look
+odd at first sight, but reflects long years of experience in getting
+system plumbing right (which is quite hard).
 
 
 Supported platforms
 -------------------
 
 The following hardware and operating system platforms are officially
-supported by the Isabelle distribution (and bundled tools):
-
-  x86-linux
-  x86-darwin
-  x86-cygwin
-  x86_64-linux
-  x86_64-darwin
+supported by the Isabelle distribution (and bundled tools), with the
+following reference versions (which have been selected to be neither
+too old nor too new):
 
-As of Cygwin 1.7 there is only a 32 bit version of that platform.  The
-other 64 bit platforms become more and more important for power users
-and always need to be taken into account when testing tools.
+  x86-linux         Ubuntu 8.04 LTS Server
+  x86-darwin        Mac OS Leopard
+  x86-cygwin        Cygwin 1.7
 
-All of the above platforms are 100% supported -- end-users should not
-have to care about the differences at all.  There are also some
-secondary platforms where Poly/ML also happens to work:
+  x86_64-linux      Ubuntu 8.04 LTS Server (64)
+  x86_64-darwin     Mac OS Leopard
+
+All of the above platforms are 100% supported by Isabelle -- end-users
+should not have to care about the differences at all.  There are also
+some secondary platforms where Poly/ML also happens to work:
 
   ppc-darwin
   sparc-solaris
@@ -45,7 +47,27 @@
 
 There is no guarantee that Isabelle add-ons work on these fringe
 platforms.  Even Isabelle/Scala already fails on ppc-darwin due to
-lack of JVM 1.6 support on that platform.
+lack of JVM 1.6 support by Apple.
+
+
+32 bit vs. 64 bit platforms
+---------------------------
+
+64 bit hardware becomes more and more important for power users.
+Add-on tools need to work seamlessly without manual user
+configuration, although it is often sufficient to fall back on 32 bit
+executables.
+
+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 expressions 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 the the respective binaries that are actually run.
 
 
 Dependable system tools
@@ -53,17 +75,17 @@
 
 The following portable system tools can be taken for granted:
 
-  * GNU bash as uniform shell on all platforms.  Note that the POSIX
-    "standard" shell /bin/sh is *not* appropriate, because there are
-    too many different implementations of it.
+* GNU bash as uniform shell on all platforms.  The POSIX "standard"
+  shell /bin/sh is *not* appropriate, because there are too many
+  different implementations of it.
 
-  * Perl as largely portable system programming language.  In some
-    situations Python may as an alternative, but it usually performs
-    not as well in addressing various delicate details of basic
-    operating system concepts (processes, signals, sockets etc.).
+* Perl as largely portable system programming language.  In some
+  situations Python may serve as an alternative, but it usually
+  performs not as well in addressing various delicate details of
+  operating system concepts (processes, signals, sockets etc.).
 
-  * Scala with Java Runtime 1.6.  The Isabelle/Pure.jar library irons
-    out many oddities and portability problems of the Java platform.
+* Scala with Java Runtime 1.6.  The Isabelle/Pure.jar library irons
+  out many oddities and portability problems of the Java platform.
 
 
 Known problems
@@ -71,11 +93,18 @@
 
 * Mac OS: If MacPorts is installed and its version of Perl takes
   precedence over /usr/bin/perl in the PATH, then the end-user needs
-  to take care of installing add-on modules, e.g. HTTP support.  Such
-  add-ons are usually included in Apple's /usr/bin/perl by default.
+  to take care of installing extra modules, e.g. for HTTP support.
+  Such add-ons are usually included in Apple's /usr/bin/perl by
+  default.
 
 * The Java runtime has its own idea about the underlying platform,
-  e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM
+  e.g. on a 64 bit machine Isabelle/ML could be x86-linux, but the JVM
   could be x86_64-linux.  This affects Java native libraries in
-  particular -- which are very hard to support in a platform
-  independent manner, and should be avoided in the first place.
+  particular -- which cause extra portability problems and can make
+  the JVM crash anyway.
+
+  In Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
+  platform.  Since there can be many different Java installations on
+  the same machine, which can also be run with different options,
+  reliable JVM platform identification works from inside the running
+  JVM only.
--- a/Admin/isatest/settings/cygwin-poly	Mon Apr 19 19:41:30 2010 +0200
+++ b/Admin/isatest/settings/cygwin-poly	Tue Apr 20 14:39:42 2010 +0200
@@ -22,6 +22,6 @@
 ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
-ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -v true -t true"
+ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false"
 
 init_component "$HOME/contrib_devel/kodkodi"
--- a/NEWS	Mon Apr 19 19:41:30 2010 +0200
+++ b/NEWS	Tue Apr 20 14:39:42 2010 +0200
@@ -339,6 +339,13 @@
 feature since Isabelle2009).  Use ISABELLE_PROCESS and ISABELLE_TOOL,
 respectively.
 
+* Old lib/scripts/polyml-platform is superseded by the
+ISABELLE_PLATFORM setting variable, which defaults to the 32 bit
+variant, even on a 64 bit machine.  The following example setting
+prefers 64 bit if available:
+
+  ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
+
 
 
 New in Isabelle2009-1 (December 2009)
--- a/etc/settings	Mon Apr 19 19:41:30 2010 +0200
+++ b/etc/settings	Tue Apr 20 14:39:42 2010 +0200
@@ -17,7 +17,7 @@
 
 # Poly/ML 5.x (automated settings)
 POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
-ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform")
+ML_PLATFORM="$ISABELLE_PLATFORM"
 ML_HOME=$(choosefrom \
   "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
   "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
@@ -55,7 +55,7 @@
 ### JVM components (Scala or Java)
 ###
 
-ISABELLE_JAVA="${THIS_JAVA:-java}"
+ISABELLE_JAVA="java"
 ISABELLE_SCALA="scala"
 
 [ -z "$SCALA_HOME" ] && SCALA_HOME=$(choosefrom \
--- a/lib/Tools/java	Mon Apr 19 19:41:30 2010 +0200
+++ b/lib/Tools/java	Tue Apr 20 14:39:42 2010 +0200
@@ -5,4 +5,4 @@
 # DESCRIPTION: invoke Java within the Isabelle environment
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "$ISABELLE_JAVA" "$@"
+exec "${THIS_JAVA:-ISABELLE_JAVA}" "$@"
--- a/lib/scripts/isabelle-platform	Mon Apr 19 19:41:30 2010 +0200
+++ b/lib/scripts/isabelle-platform	Tue Apr 20 14:39:42 2010 +0200
@@ -26,6 +26,10 @@
           ISABELLE_PLATFORM64=x86_64-darwin
         fi
         ;;
+      x86_64)
+        ISABELLE_PLATFORM=x86-darwin
+        ISABELLE_PLATFORM64=x86_64-darwin
+        ;;
       Power* | power* | ppc)
         ISABELLE_PLATFORM=ppc-darwin
         ;;
@@ -33,7 +37,7 @@
     ;;
   CYGWIN_NT*)
     case $(uname -m) in
-      i?86)
+      i?86 | x86_64)
         ISABELLE_PLATFORM=x86-cygwin
         ;;
     esac
@@ -45,7 +49,7 @@
           sparc)
             ISABELLE_PLATFORM=sparc-solaris
             ;;
-          i?86)
+          i?86 | x86_64)
             ISABELLE_PLATFORM=x86-solaris
             ;;
         esac
@@ -54,7 +58,7 @@
     ;;
   FreeBSD|NetBSD)
     case $(uname -m) in
-      i?86)
+      i?86 | x86_64)
         ISABELLE_PLATFORM=x86-bsd
         ;;
     esac
--- a/lib/scripts/polyml-platform	Mon Apr 19 19:41:30 2010 +0200
+++ b/lib/scripts/polyml-platform	Tue Apr 20 14:39:42 2010 +0200
@@ -1,69 +1,4 @@
 #!/usr/bin/env bash
-#
-# polyml-platform --- determine Poly/ML's idea of current hardware and
-# operating system type
-#
-# NOTE: platform identifiers should be kept as generic as possible,
-# i.e. shared by compatible environments.
-
-PLATFORM="unknown-platform"
 
-case $(uname -s) in
-  SunOS)
-    case $(uname -r) in
-      5.*)
-        case $(uname -p) in
-          sparc)
-            PLATFORM=sparc-solaris
-            ;;
-          i?86)
-            PLATFORM=x86-solaris
-            ;;
-        esac
-        ;;
-    esac
-    ;;
-  Linux)
-    case $(uname -m) in
-      i?86 | x86_64)
-        PLATFORM=x86-linux
-        ;;
-      Power* | power* | ppc)
-        PLATFORM=ppc-linux
-        ;;
-    esac
-    ;;
-  FreeBSD|NetBSD)
-    case $(uname -m) in
-      i?86)
-        PLATFORM=x86-bsd
-        ;;
-    esac
-    ;;
-  Darwin)
-    case $(uname -m) in
-      Power* | power* | ppc)
-        PLATFORM=ppc-darwin
-        ;;
-      i?86)
-        PLATFORM=x86-darwin
-        ;;
-    esac
-    ;;
-  CYGWIN_NT*)
-    case $(uname -m) in
-      i?86)
-        PLATFORM=x86-cygwin
-        ;;
-    esac
-    ;;
-  Windows_NT)
-    case $(uname -m) in
-      ?86)
-        PLATFORM=x86-win32
-        ;;
-    esac
-    ;;
-esac
-
-echo "$PLATFORM"
+echo "### Legacy feature: polyml-platform script is superseded by ISABELLE_PLATFORM" >&2
+echo "$ISABELLE_PLATFORM"
--- a/src/Pure/Isar/code.ML	Mon Apr 19 19:41:30 2010 +0200
+++ b/src/Pure/Isar/code.ML	Tue Apr 20 14:39:42 2010 +0200
@@ -35,8 +35,8 @@
   val cert_of_eqns: theory -> string -> (thm * bool) list -> cert
   val constrain_cert: theory -> sort list -> cert -> cert
   val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list
-  val equations_of_cert: theory -> cert ->
-    ((string * sort) list * typ) * ((string option * (term list * term)) * (thm option * bool)) list
+  val equations_of_cert: theory -> cert -> ((string * sort) list * typ)
+    * (((term * string option) list * (term * string option)) * (thm option * bool)) list
   val bare_thms_of_cert: theory -> cert -> thm list
   val pretty_cert: theory -> cert -> Pretty.T list
 
@@ -461,6 +461,16 @@
   in not (has_duplicates (op =) ((fold o fold_aterms)
     (fn Var (v, _) => cons v | _ => I) args [])) end;
 
+fun check_decl_ty thy (c, ty) =
+  let
+    val ty_decl = Sign.the_const_type thy c;
+  in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) then ()
+    else bad_thm ("Type\n" ^ string_of_typ thy ty
+      ^ "\nof constant " ^ quote c
+      ^ "\nis incompatible with declared type\n"
+      ^ string_of_typ thy ty_decl)
+  end; 
+
 fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) =
   let
     fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
@@ -496,7 +506,7 @@
               then ()
               else bad (quote c ^ " is not a constructor, on left hand side of equation")
             else bad ("Partially applied constant " ^ quote c ^ " on left hand side of equation")
-          end else bad ("Pattern not allowed, but constant " ^ quote c ^ " encountered on left hand side")
+          end else bad ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side")
     val _ = map (check 0) args;
     val _ = if allow_nonlinear orelse is_linear thm then ()
       else bad "Duplicate variables on left hand side of equation";
@@ -506,13 +516,7 @@
       else bad "Constructor as head in equation";
     val _ = if not (is_abstr thy c) then ()
       else bad "Abstractor as head in equation";
-    val ty_decl = Sign.the_const_type thy c;
-    val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
-      then () else bad_thm ("Type\n" ^ string_of_typ thy ty
-        ^ "\nof equation\n"
-        ^ Display.string_of_thm_global thy thm
-        ^ "\nis incompatible with declared function type\n"
-        ^ string_of_typ thy ty_decl)
+    val _ = check_decl_ty thy (c, ty);
   in () end;
 
 fun gen_assert_eqn thy check_patterns (thm, proper) =
@@ -533,17 +537,19 @@
            | THM _ => bad "Not a proper equation";
     val (rep, lhs) = dest_comb full_lhs
       handle TERM _ => bad "Not an abstract equation";
-    val tyco = (fst o dest_Type o domain_type o snd o dest_Const) rep
+    val (rep_const, ty) = dest_Const rep;
+    val (tyco, sorts) = ((apsnd o map) (snd o dest_TVar) o dest_Type o domain_type) ty
       handle TERM _ => bad "Not an abstract equation";
     val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
           else bad ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
       | NONE => ();
-    val (_, (_, (rep', _))) = get_abstype_spec thy tyco;
-    val rep_const = (fst o dest_Const) rep;
+    val (vs', (_, (rep', _))) = get_abstype_spec thy tyco;
     val _ = if rep_const = rep' then ()
       else bad ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
     val _ = check_eqn thy { allow_nonlinear = false,
       allow_consts = false, allow_pats = false } thm (lhs, rhs);
+    val _ = if forall (Sign.subsort thy) (sorts ~~ map snd  vs') then ()
+      else error ("Sort constraints on type arguments are weaker than in abstype certificate.")
   in (thm, tyco) end;
 
 fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
@@ -643,19 +649,21 @@
 
 fun check_abstype_cert thy proto_thm =
   let
-    val thm = meta_rewrite thy proto_thm;
+    val thm = (AxClass.unoverload thy o meta_rewrite thy) proto_thm;
     fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
     val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
       handle TERM _ => bad "Not an equation"
            | THM _ => bad "Not a proper equation";
-    val ((abs, raw_ty), ((rep, _), param)) = (apsnd (apfst dest_Const o dest_comb)
+    val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb)
         o apfst dest_Const o dest_comb) lhs
       handle TERM _ => bad "Not an abstype certificate";
+    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
+      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
+    val _ = check_decl_ty thy (abs, raw_ty);
+    val _ = check_decl_ty thy (rep, rep_ty);
     val var = (fst o dest_Var) param
       handle TERM _ => bad "Not an abstype certificate";
     val _ = if param = rhs then () else bad "Not an abstype certificate";
-    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
-      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
     val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
     val ty = domain_type ty';
     val ty_abs = range_type ty';
@@ -809,7 +817,7 @@
       let
         val vs = fst (typscheme_abs thy abs_thm);
         val (_, concrete_thm) = concretify_abs thy tyco abs_thm;
-      in (vs, add_rhss_of_eqn thy (Thm.prop_of abs_thm) []) end;
+      in (vs, add_rhss_of_eqn thy (map_types Logic.unvarifyT_global (Thm.prop_of concrete_thm)) []) end;
 
 fun equations_of_cert thy (cert as Equations (cert_thm, propers)) =
       let
@@ -819,22 +827,23 @@
           |> Local_Defs.expand [snd (get_head thy cert_thm)]
           |> Thm.varifyT_global
           |> Conjunction.elim_balanced (length propers);
-      in (tyscm, map (pair NONE o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
+        fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, NONE));
+      in (tyscm, map (abstractions o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
   | equations_of_cert thy (Projection (t, tyco)) =
       let
         val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
         val tyscm = typscheme_projection thy t;
         val t' = map_types Logic.varifyT_global t;
-      in (tyscm, [((SOME abs, dest_eqn thy t'), (NONE, true))]) end
+        fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE));
+      in (tyscm, [((abstractions o dest_eqn thy) t', (NONE, true))]) end
   | equations_of_cert thy (Abstract (abs_thm, tyco)) =
       let
         val tyscm = typscheme_abs thy abs_thm;
         val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
-        val _ = fold_aterms (fn Const (c, _) => if c = abs
-          then error ("Abstraction violation in abstract code equation\n" ^ Display.string_of_thm_global thy abs_thm)
-          else I | _ => I) (Thm.prop_of abs_thm);
+        fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, (SOME abs)));
       in
-        (tyscm, [((SOME abs, dest_eqn thy (Thm.prop_of concrete_thm)), (SOME (Thm.varifyT_global abs_thm), true))])
+        (tyscm, [((abstractions o dest_eqn thy o Thm.prop_of) concrete_thm,
+          (SOME (Thm.varifyT_global abs_thm), true))])
       end;
 
 fun pretty_cert thy (cert as Equations _) =
@@ -1109,12 +1118,13 @@
     val (old_constrs, some_old_proj) =
       case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
        of (_, (_, Constructors cos)) :: _ => (map fst cos, NONE)
-        | (_, (_, Abstractor (_, (co, _)))) :: _ => ([], SOME co)
+        | (_, (_, Abstractor ((co, _), (proj, _)))) :: _ => ([co], SOME proj)
         | [] => ([], NONE)
     val outdated_funs = case some_old_proj
      of NONE => old_constrs
       | SOME old_proj => Symtab.fold
-          (fn (c, ((_, spec), _)) => if member (op =) (the_list (associated_abstype spec)) tyco
+          (fn (c, ((_, spec), _)) =>
+            if member (op =) (the_list (associated_abstype spec)) tyco
             then insert (op =) c else I)
             ((the_functions o the_exec) thy) (old_proj :: old_constrs);
     fun drop_outdated_cases cases = fold Symtab.delete_safe
@@ -1160,7 +1170,7 @@
 fun add_abstype proto_thm thy =
   let
     val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert)))) =
-      check_abstype_cert thy proto_thm;
+      error_thm (check_abstype_cert thy) proto_thm;
   in
     thy
     |> del_eqns abs
--- a/src/Pure/Syntax/syntax.ML	Mon Apr 19 19:41:30 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Apr 20 14:39:42 2010 +0200
@@ -290,15 +290,14 @@
     val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2,
       parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
       print_ast_translation, token_translation} = syn_ext;
-    val input' = if inout then fold (insert (op =)) xprods input else input;
-    val changed = length input <> length input';
+    val new_xprods =
+      if inout then distinct (op =) (filter_out (member (op =) input) xprods) else [];
     fun if_inout xs = if inout then xs else [];
   in
     Syntax
-    ({input = input',
-      lexicon =
-        if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
-      gram = if changed then Parser.extend_gram gram xprods else gram,
+    ({input = new_xprods @ input,
+      lexicon = fold Scan.extend_lexicon (SynExt.delims_of new_xprods) lexicon,
+      gram = Parser.extend_gram gram new_xprods,
       consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
       prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
       parse_ast_trtab =
--- a/src/Pure/System/gui_setup.scala	Mon Apr 19 19:41:30 2010 +0200
+++ b/src/Pure/System/gui_setup.scala	Tue Apr 20 14:39:42 2010 +0200
@@ -43,15 +43,16 @@
     }
 
     // values
-    text.append("JVM platform: " + Platform.jvm_platform() + "\n")
     if (Platform.is_windows)
       text.append("Cygwin root: " + Cygwin.check_root() + "\n")
+    text.append("JVM platform: " + Platform.jvm_platform + "\n")
     try {
       val isabelle_system = new Isabelle_System
-      text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
+      text.append("ML platform: " + isabelle_system.getenv("ML_PLATFORM") + "\n")
       text.append("Isabelle platform: " + isabelle_system.getenv("ISABELLE_PLATFORM") + "\n")
       val platform64 = isabelle_system.getenv("ISABELLE_PLATFORM64")
       if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
+      text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
       text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
     } catch {
       case e: RuntimeException => text.append(e.getMessage + "\n")
--- a/src/Pure/System/platform.scala	Mon Apr 19 19:41:30 2010 +0200
+++ b/src/Pure/System/platform.scala	Tue Apr 20 14:39:42 2010 +0200
@@ -31,7 +31,7 @@
   private val Sparc = new Regex("sparc")
   private val PPC = new Regex("PowerPC|ppc")
 
-  def jvm_platform(): String =
+  lazy val jvm_platform: String =
   {
     val arch =
       java.lang.System.getProperty("os.arch") match {
--- a/src/Tools/Code/code_thingol.ML	Mon Apr 19 19:41:30 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Apr 20 14:39:42 2010 +0200
@@ -655,10 +655,10 @@
             translate_app thy algbr eqngr some_abs some_thm ((c, ty), ts)
         | (t', ts) =>
             translate_term thy algbr eqngr some_abs some_thm t'
-            ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
+            ##>> fold_map (translate_term thy algbr eqngr NONE some_thm) ts
             #>> (fn (t, ts) => t `$$ ts)
-and translate_eqn thy algbr eqngr ((some_abs, (args, rhs)), (some_thm, proper)) =
-  fold_map (translate_term thy algbr eqngr some_abs some_thm) args
+and translate_eqn thy algbr eqngr ((args, (rhs, some_abs)), (some_thm, proper)) =
+  fold_map (fn (arg, some_abs) => translate_term thy algbr eqngr some_abs some_thm arg) args
   ##>> translate_term thy algbr eqngr some_abs some_thm rhs
   #>> rpair (some_thm, proper)
 and translate_const thy algbr eqngr some_abs some_thm (c, ty) =
@@ -680,7 +680,7 @@
   end
 and translate_app_const thy algbr eqngr some_abs some_thm (c_ty, ts) =
   translate_const thy algbr eqngr some_abs some_thm c_ty
-  ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
+  ##>> fold_map (translate_term thy algbr eqngr NONE some_thm) ts
   #>> (fn (t, ts) => t `$$ ts)
 and translate_case thy algbr eqngr some_abs some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   let
@@ -753,7 +753,7 @@
     translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), ts)
 and translate_app thy algbr eqngr some_abs some_thm (c_ty_ts as ((c, _), _)) =
   case Code.get_case_scheme thy c
-   of SOME case_scheme => translate_app_case thy algbr eqngr some_abs some_thm case_scheme c_ty_ts
+   of SOME case_scheme => translate_app_case thy algbr eqngr NONE some_thm case_scheme c_ty_ts
     | NONE => translate_app_const thy algbr eqngr some_abs some_thm c_ty_ts
 and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr (v, sort) =
   fold_map (ensure_class thy algbr eqngr) (proj_sort sort)