# HG changeset patch
# User blanchet
# Date 1409581066 -7200
# Node ID ab6220d6cf70821f287c8e054f0c8a34611e987c
# Parent  8081087096add2b466380c899fc381a4889eed8f
tuning

diff -r 8081087096ad -r ab6220d6cf70 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -31,14 +31,14 @@
     fun perm_dtyp (Old_Datatype_Aux.DtType (s, Ds)) = Old_Datatype_Aux.DtType (s, map perm_dtyp Ds)
       | perm_dtyp (Old_Datatype_Aux.DtRec kk) =
         Old_Datatype_Aux.DtRec (find_index (curry (op =) kk) kks)
-      | perm_dtyp D = D
+      | perm_dtyp D = D;
   in
     if perm_kks = kks then
       desc
     else
       perm_kks ~~
       map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc
-  end
+  end;
 
 (* TODO: graceful failure for local datatypes -- perhaps by making the command global *)
 fun datatype_compat_cmd raw_fpT_names0 lthy =
@@ -177,7 +177,7 @@
 
     val register_interpret =
       Old_Datatype_Data.register infos
-      #> Old_Datatype_Data.interpretation_data (Old_Datatype_Aux.default_config, map fst infos)
+      #> Old_Datatype_Data.interpretation_data (Old_Datatype_Aux.default_config, map fst infos);
   in
     lthy
     |> Local_Theory.raw_theory register_interpret