src/Pure/Isar/generic_target.ML

   val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   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
 
 (** lifting primitive to target operations **)

     val params = type_params @ term_params;
 
     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
       |> Local_Defs.add_def ((b, NoSyn), lhs');
     val def = Local_Defs.trans_terms lthy3