tuned;
authorwenzelm
Thu Oct 11 15:06:27 2012 +0200 (2012-10-11)
changeset 4981785b37aece3b3
parent 49816 e63d6c55ad6d
child 49818 db42a1147986
tuned;
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Oct 11 12:38:18 2012 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Oct 11 15:06:27 2012 +0200
     1.3 @@ -144,13 +144,14 @@
     1.4  local
     1.5  
     1.6  fun prep_inst prep_term ctxt parms (Positional insts) =
     1.7 -      (insts ~~ parms) |> map (fn
     1.8 -        (NONE, p) => Free (p, dummyT) |
     1.9 -        (SOME t, _) => prep_term ctxt t)
    1.10 +      (insts ~~ parms) |> map
    1.11 +        (fn (NONE, p) => Free (p, dummyT)
    1.12 +          | (SOME t, _) => prep_term ctxt t)
    1.13    | prep_inst prep_term ctxt parms (Named insts) =
    1.14 -      parms |> map (fn p => case AList.lookup (op =) insts p of
    1.15 -        SOME t => prep_term ctxt t |
    1.16 -        NONE => Free (p, dummyT));
    1.17 +      parms |> map (fn p =>
    1.18 +        (case AList.lookup (op =) insts p of
    1.19 +          SOME t => prep_term ctxt t |
    1.20 +          NONE => Free (p, dummyT)));
    1.21  
    1.22  in
    1.23  
    1.24 @@ -286,6 +287,16 @@
    1.25  
    1.26  (** Finish locale elements **)
    1.27  
    1.28 +fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
    1.29 +      let val x = Binding.name_of binding
    1.30 +      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
    1.31 +  | finish_primitive _ _ (Constrains _) = Constrains []
    1.32 +  | finish_primitive _ close (Assumes asms) = close (Assumes asms)
    1.33 +  | finish_primitive _ close (Defines defs) = close (Defines defs)
    1.34 +  | finish_primitive _ _ (Notes facts) = Notes facts;
    1.35 +
    1.36 +local
    1.37 +
    1.38  fun closeup _ _ false elem = elem
    1.39    | closeup ctxt parms true elem =
    1.40        let
    1.41 @@ -309,13 +320,8 @@
    1.42          | e => e)
    1.43        end;
    1.44  
    1.45 -fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
    1.46 -      let val x = Binding.name_of binding
    1.47 -      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
    1.48 -  | finish_primitive _ _ (Constrains _) = Constrains []
    1.49 -  | finish_primitive _ close (Assumes asms) = close (Assumes asms)
    1.50 -  | finish_primitive _ close (Defines defs) = close (Defines defs)
    1.51 -  | finish_primitive _ _ (Notes facts) = Notes facts;
    1.52 +fun finish_elem ctxt parms do_close elem =
    1.53 +  finish_primitive parms (closeup ctxt parms do_close) elem;
    1.54  
    1.55  fun finish_inst ctxt (loc, (prfx, inst)) =
    1.56    let
    1.57 @@ -324,8 +330,7 @@
    1.58      val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
    1.59    in (loc, morph) end;
    1.60  
    1.61 -fun finish_elem ctxt parms do_close elem =
    1.62 -  finish_primitive parms (closeup ctxt parms do_close) elem;
    1.63 +in
    1.64  
    1.65  fun finish ctxt parms do_close insts elems =
    1.66    let
    1.67 @@ -333,6 +338,8 @@
    1.68      val elems' = map (finish_elem ctxt parms do_close) elems;
    1.69    in (deps, elems') end;
    1.70  
    1.71 +end;
    1.72 +
    1.73  
    1.74  (** Process full context statement: instantiations + elements + conclusion **)
    1.75  
    1.76 @@ -428,12 +435,12 @@
    1.77  
    1.78  fun prep_statement prep activate raw_elems raw_concl context =
    1.79    let
    1.80 -     val ((_, _, elems, concl), _) =
    1.81 -       prep {strict = true, do_close = false, fixed_frees = true}
    1.82 +    val ((_, _, elems, concl), _) =
    1.83 +      prep {strict = true, do_close = false, fixed_frees = true}
    1.84          ([], []) I raw_elems raw_concl context;
    1.85 -     val (_, context') = context |>
    1.86 -       Proof_Context.set_stmt true |>
    1.87 -       fold_map activate elems;
    1.88 +    val (_, context') = context
    1.89 +      |> Proof_Context.set_stmt true
    1.90 +      |> fold_map activate elems;
    1.91    in (concl, context') end;
    1.92  
    1.93  in