# HG changeset patch
# User blanchet
# Date 1383565228 -3600
# Node ID 99ef8036fb3d180f405cafa79adbf867a266ed6a
# Parent  357988ad95ec0bb0be6203769750d2b58499f7f4
tuning

diff -r 357988ad95ec -r 99ef8036fb3d src/HOL/BNF/Tools/bnf_fp_n2m.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Mon Nov 04 11:59:08 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Mon Nov 04 12:40:28 2013 +0100
@@ -376,6 +376,6 @@
        |> morph_fp_result (Morphism.term_morphism (singleton (Variable.polymorphic lthy))));
   in
     (fp_res, lthy)
-  end
+  end;
 
 end;