# HG changeset patch # User blanchet # Date 1271767182 -7200 # Node ID 77abfa526524a0b903a20d42f08df46d63287e98 # Parent 1263bef003b3ff3cc235f725cf4f9041055339b8# Parent 4df49260bd82a92e2505d0ace9f323637520d488 merge diff -r 1263bef003b3 -r 77abfa526524 Admin/PLATFORMS --- 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. diff -r 1263bef003b3 -r 77abfa526524 Admin/isatest/settings/cygwin-poly --- 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" diff -r 1263bef003b3 -r 77abfa526524 NEWS --- 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) diff -r 1263bef003b3 -r 77abfa526524 etc/settings --- 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 \ diff -r 1263bef003b3 -r 77abfa526524 lib/Tools/java --- 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}" "$@" diff -r 1263bef003b3 -r 77abfa526524 lib/scripts/isabelle-platform --- 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 diff -r 1263bef003b3 -r 77abfa526524 lib/scripts/polyml-platform --- 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" diff -r 1263bef003b3 -r 77abfa526524 src/Pure/Isar/code.ML --- 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 diff -r 1263bef003b3 -r 77abfa526524 src/Pure/Syntax/syntax.ML --- 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 = diff -r 1263bef003b3 -r 77abfa526524 src/Pure/System/gui_setup.scala --- 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") diff -r 1263bef003b3 -r 77abfa526524 src/Pure/System/platform.scala --- 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 { diff -r 1263bef003b3 -r 77abfa526524 src/Tools/Code/code_thingol.ML --- 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)