# 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;