refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x";
authorwenzelm
Thu Oct 11 16:09:44 2012 +0200 (2012-10-11)
changeset 4981997b572c10fe9
parent 49818 db42a1147986
child 49820 f7a1e1745b7b
refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x";
tuned;
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Oct 11 15:26:33 2012 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Oct 11 16:09:44 2012 +0200
     1.3 @@ -287,6 +287,13 @@
     1.4  
     1.5  (** Finish locale elements **)
     1.6  
     1.7 +fun finish_inst ctxt (loc, (prfx, inst)) =
     1.8 +  let
     1.9 +    val thy = Proof_Context.theory_of ctxt;
    1.10 +    val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
    1.11 +    val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
    1.12 +  in (loc, morph) end;
    1.13 +
    1.14  fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
    1.15    let val x = Binding.name_of binding
    1.16    in (binding, AList.lookup (op =) parms x, mx) end);
    1.17 @@ -294,14 +301,15 @@
    1.18  local
    1.19  
    1.20  fun closeup _ _ false elem = elem
    1.21 -  | closeup ctxt parms true elem =
    1.22 +  | closeup (outer_ctxt, ctxt) parms true elem =
    1.23        let
    1.24          (* FIXME consider closing in syntactic phase -- before type checking *)
    1.25          fun close_frees t =
    1.26            let
    1.27              val rev_frees =
    1.28                Term.fold_aterms (fn Free (x, T) =>
    1.29 -                if AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t [];
    1.30 +                if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I
    1.31 +                else insert (op =) (x, T) | _ => I) t [];
    1.32            in fold (Logic.all o Free) rev_frees t end;
    1.33  
    1.34          fun no_binds [] = []
    1.35 @@ -316,27 +324,14 @@
    1.36          | e => e)
    1.37        end;
    1.38  
    1.39 +in
    1.40 +
    1.41  fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes)
    1.42    | finish_elem _ _ _ (Constrains _) = Constrains []
    1.43 -  | finish_elem ctxt parms do_close (Assumes asms) = closeup ctxt parms do_close (Assumes asms)
    1.44 -  | finish_elem ctxt parms do_close (Defines defs) = closeup ctxt parms do_close (Defines defs)
    1.45 +  | finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms)
    1.46 +  | finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs)
    1.47    | finish_elem _ _ _ (Notes facts) = Notes facts;
    1.48  
    1.49 -fun finish_inst ctxt (loc, (prfx, inst)) =
    1.50 -  let
    1.51 -    val thy = Proof_Context.theory_of ctxt;
    1.52 -    val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
    1.53 -    val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
    1.54 -  in (loc, morph) end;
    1.55 -
    1.56 -in
    1.57 -
    1.58 -fun finish ctxt parms do_close insts elems =
    1.59 -  let
    1.60 -    val deps = map (finish_inst ctxt) insts;
    1.61 -    val elems' = map (finish_elem ctxt parms do_close) elems;
    1.62 -  in (deps, elems') end;
    1.63 -
    1.64  end;
    1.65  
    1.66  
    1.67 @@ -407,7 +402,8 @@
    1.68  
    1.69      val fors' = finish_fixes parms fors;
    1.70      val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
    1.71 -    val (deps, elems'') = finish ctxt6 parms do_close insts elems';
    1.72 +    val deps = map (finish_inst ctxt6) insts;
    1.73 +    val elems'' = map (finish_elem (ctxt1, ctxt6) parms do_close) elems';
    1.74  
    1.75    in ((fixed, deps, elems'', concl), (parms, ctxt7)) end
    1.76