# HG changeset patch
# User haftmann
# Date 1501757401 -7200
# Node ID a0369be639486f03c299de21bb491219a36c1ab4
# Parent  cf9ce8016da1d49ad83352181601eba4ea63353c
uniform namespace handling for both concrete and abstract types, following 32e0da92c786

diff -r cf9ce8016da1 -r a0369be63948 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Aug 03 12:50:00 2017 +0200
+++ b/src/Pure/Isar/code.ML	Thu Aug 03 12:50:01 2017 +0200
@@ -1298,18 +1298,21 @@
     |> map_types (History.register tyco vs_typ_spec)
   end;
 
+fun type_interpretation get_spec tyco f =
+  Local_Theory.background_theory (fn thy =>
+    thy
+    |> Sign.root_path
+    |> Sign.add_path (Long_Name.qualifier tyco)
+    |> f (tyco, get_spec thy tyco)
+    |> Sign.restore_naming thy);
+
 structure Datatype_Plugin = Plugin(type T = string);
 
 val datatype_plugin = Plugin_Name.declare_setup @{binding datatype_code};
 
 fun datatype_interpretation f =
   Datatype_Plugin.interpretation datatype_plugin
-    (fn tyco => Local_Theory.background_theory (fn thy =>
-      thy
-      |> Sign.root_path
-      |> Sign.add_path (Long_Name.qualifier tyco)
-      |> f (tyco, fst (get_type thy tyco))
-      |> Sign.restore_naming thy));
+    (fn tyco => type_interpretation (fst oo get_type) tyco f);
 
 fun declare_datatype_global proto_constrs thy =
   let
@@ -1333,8 +1336,7 @@
 
 fun abstype_interpretation f =
   Abstype_Plugin.interpretation abstype_plugin
-    (fn tyco =>
-      Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy));
+    (fn tyco => type_interpretation get_abstype_spec tyco f);
 
 fun generic_declare_abstype strictness proto_thm thy =
   case check_abstype_cert strictness thy proto_thm of