tuned;

--- a/src/Pure/Isar/generic_target.ML	Sat Nov 05 22:01:19 2011 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sat Nov 05 22:41:25 2011 +0100
@@ -26,7 +26,7 @@
   val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
     local_theory -> local_theory
   val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
-end;
+end
 
 structure Generic_Target: GENERIC_TARGET =
 struct
@@ -77,8 +77,8 @@
     val U = map Term.fastype_of params ---> T;
 
     (*foundation*)
-    val ((lhs', global_def), lthy2) = foundation
-      (((b, U), mx'), (b_def, rhs')) (type_params, term_params) lthy;
+    val ((lhs', global_def), lthy2) = lthy
+      |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params);
 
     (*local definition*)
     val ((lhs, local_def), lthy3) = lthy2

--- a/src/Pure/Isar/named_target.ML	Sat Nov 05 22:01:19 2011 +0100
+++ b/src/Pure/Isar/named_target.ML	Sat Nov 05 22:41:25 2011 +0100
@@ -158,10 +158,12 @@
     val target_name =
       [Pretty.command (if is_class then "class" else "locale"),
         Pretty.str (" " ^ Locale.extern thy target)];
-    val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
-      (#1 (Proof_Context.inferred_fixes ctxt));
-    val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
-      (Assumption.all_assms_of ctxt);
+    val fixes =
+      map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
+        (#1 (Proof_Context.inferred_fixes ctxt));
+    val assumes =
+      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
+        (Assumption.all_assms_of ctxt);
     val elems =
       (if null fixes then [] else [Element.Fixes fixes]) @
       (if null assumes then [] else [Element.Assumes assumes]);