--- a/src/Pure/Isar/expression.ML Sun Mar 29 18:06:14 2009 +0200
+++ b/src/Pure/Isar/expression.ML Sun Mar 29 19:41:04 2009 +0200
@@ -70,12 +70,12 @@
fun intern thy instances = map (apfst (Locale.intern thy)) instances;
-(** Parameters of expression.
+(** Parameters of expression **)
- Sanity check of instantiations and extraction of implicit parameters.
- The latter only occurs iff strict = false.
- Positional instantiations are extended to match full length of parameter list
- of instantiated locale. **)
+(*Sanity check of instantiations and extraction of implicit parameters.
+ The latter only occurs iff strict = false.
+ Positional instantiations are extended to match full length of parameter list
+ of instantiated locale.*)
fun parameters_of thy strict (expr, fixed) =
let
@@ -88,7 +88,7 @@
(mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
- fun params_inst (expr as (loc, (prfx, Positional insts))) =
+ fun params_inst (loc, (prfx, Positional insts)) =
let
val ps = params_loc loc;
val d = length ps - length insts;
@@ -99,24 +99,22 @@
val ps' = (ps ~~ insts') |>
map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
in (ps', (loc, (prfx, Positional insts'))) end
- | params_inst (expr as (loc, (prfx, Named insts))) =
+ | params_inst (loc, (prfx, Named insts)) =
let
val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
(map fst insts);
-
- val ps = params_loc loc;
- val ps' = fold (fn (p, _) => fn ps =>
+ val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
if AList.defined (op =) ps p then AList.delete (op =) p ps
- else error (quote p ^ " not a parameter of instantiated expression")) insts ps;
+ else error (quote p ^ " not a parameter of instantiated expression"));
in (ps', (loc, (prfx, Named insts))) end;
fun params_expr is =
+ let
+ val (is', ps') = fold_map (fn i => fn ps =>
let
- val (is', ps') = fold_map (fn i => fn ps =>
- let
- val (ps', i') = params_inst i;
- val ps'' = distinct parm_eq (ps @ ps');
- in (i', ps'') end) is []
- in (ps', is') end;
+ val (ps', i') = params_inst i;
+ val ps'' = distinct parm_eq (ps @ ps');
+ in (i', ps'') end) is []
+ in (ps', is') end;
val (implicit, expr') = params_expr expr;
@@ -343,7 +341,7 @@
val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
- fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
+ fun prep_insts_cumulative (loc, (prfx, inst)) (i, insts, ctxt) =
let
val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
val inst' = prep_inst ctxt parm_names inst;
@@ -361,7 +359,7 @@
let
val ctxt' = declare_elem prep_vars_elem raw_elem ctxt;
val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
- val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
+ val (_, _, _, ctxt'' (* FIXME not used *) ) = check_autofix insts elems' [] ctxt';
in (elems', ctxt') end;
fun prep_concl raw_concl (insts, elems, ctxt) =
@@ -371,11 +369,10 @@
val fors = prep_vars_inst fixed ctxt1 |> fst;
val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
- val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
+ val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
val ctxt4 = init_body ctxt3;
val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
- val (insts, elems', concl, ctxt6) =
- prep_concl raw_concl (insts', elems, ctxt5);
+ val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
(* Retrieve parameter types *)
val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes)