# HG changeset patch
# User haftmann
# Date 1496690680 -7200
# Node ID 22ef720a92b0138b69698583de62febcff2dcaff
# Parent  cc8e9289a6c403307a8a5c09367804d5e7138c1f
tuned

diff -r cc8e9289a6c4 -r 22ef720a92b0 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Jun 05 21:24:39 2017 +0200
+++ b/src/Pure/Isar/code.ML	Mon Jun 05 21:24:40 2017 +0200
@@ -1265,8 +1265,6 @@
         #> (map_cases o apfst) drop_outdated_cases)
   end;
 
-fun unoverload_const_typ thy (c, ty) = (Axclass.unoverload_const thy (c, ty), ty);
-
 structure Datatype_Plugin = Plugin(type T = string);
 
 val datatype_plugin = Plugin_Name.declare_setup @{binding datatype_code};
@@ -1282,7 +1280,9 @@
 
 fun add_datatype proto_constrs thy =
   let
-    val constrs = map (unoverload_const_typ thy) proto_constrs;
+    fun unoverload_const_typ (c, ty) =
+      (Axclass.unoverload_const thy (c, ty), ty);
+    val constrs = map unoverload_const_typ proto_constrs;
     val (tyco, (vs, cos)) = constrset_of_consts thy constrs;
   in
     thy