--- 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)