src/HOL/Tools/BNF/bnf_lfp.ML

       in
         fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
       end;
 
     val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
-        lthy
-        |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
-        ||> `Local_Theory.restore;
+      lthy
+      |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
+      ||> `Local_Theory.restore;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
     val alg_def = mk_unabs_def (2 * n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);