tuned;

--- a/src/Pure/Isar/expression.ML	Thu Oct 11 12:38:18 2012 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Oct 11 15:06:27 2012 +0200
@@ -144,13 +144,14 @@
 local
 
 fun prep_inst prep_term ctxt parms (Positional insts) =
-      (insts ~~ parms) |> map (fn
-        (NONE, p) => Free (p, dummyT) |
-        (SOME t, _) => prep_term ctxt t)
+      (insts ~~ parms) |> map
+        (fn (NONE, p) => Free (p, dummyT)
+          | (SOME t, _) => prep_term ctxt t)
   | prep_inst prep_term ctxt parms (Named insts) =
-      parms |> map (fn p => case AList.lookup (op =) insts p of
-        SOME t => prep_term ctxt t |
-        NONE => Free (p, dummyT));
+      parms |> map (fn p =>
+        (case AList.lookup (op =) insts p of
+          SOME t => prep_term ctxt t |
+          NONE => Free (p, dummyT)));
 
 in
 
@@ -286,6 +287,16 @@
 
 (** Finish locale elements **)
 
+fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
+      let val x = Binding.name_of binding
+      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
+  | finish_primitive _ _ (Constrains _) = Constrains []
+  | finish_primitive _ close (Assumes asms) = close (Assumes asms)
+  | finish_primitive _ close (Defines defs) = close (Defines defs)
+  | finish_primitive _ _ (Notes facts) = Notes facts;
+
+local
+
 fun closeup _ _ false elem = elem
   | closeup ctxt parms true elem =
       let
@@ -309,13 +320,8 @@
         | e => e)
       end;
 
-fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
-      let val x = Binding.name_of binding
-      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
-  | finish_primitive _ _ (Constrains _) = Constrains []
-  | finish_primitive _ close (Assumes asms) = close (Assumes asms)
-  | finish_primitive _ close (Defines defs) = close (Defines defs)
-  | finish_primitive _ _ (Notes facts) = Notes facts;
+fun finish_elem ctxt parms do_close elem =
+  finish_primitive parms (closeup ctxt parms do_close) elem;
 
 fun finish_inst ctxt (loc, (prfx, inst)) =
   let
@@ -324,8 +330,7 @@
     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   in (loc, morph) end;
 
-fun finish_elem ctxt parms do_close elem =
-  finish_primitive parms (closeup ctxt parms do_close) elem;
+in
 
 fun finish ctxt parms do_close insts elems =
   let
@@ -333,6 +338,8 @@
     val elems' = map (finish_elem ctxt parms do_close) elems;
   in (deps, elems') end;
 
+end;
+
 
 (** Process full context statement: instantiations + elements + conclusion **)
 
@@ -428,12 +435,12 @@
 
 fun prep_statement prep activate raw_elems raw_concl context =
   let
-     val ((_, _, elems, concl), _) =
-       prep {strict = true, do_close = false, fixed_frees = true}
+    val ((_, _, elems, concl), _) =
+      prep {strict = true, do_close = false, fixed_frees = true}
         ([], []) I raw_elems raw_concl context;
-     val (_, context') = context |>
-       Proof_Context.set_stmt true |>
-       fold_map activate elems;
+    val (_, context') = context
+      |> Proof_Context.set_stmt true
+      |> fold_map activate elems;
   in (concl, context') end;
 
 in