# HG changeset patch
# User wenzelm
# Date 1537783637 -7200
# Node ID 1ad2897ba24432c48404211da8075bc58a5124ce
# Parent  f79aeac59e1508d7a997148ebb6226e12cf959f6
eliminated dead code (see b806a7678083);

diff -r f79aeac59e15 -r 1ad2897ba244 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Sep 24 11:58:07 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Sep 24 12:07:17 2018 +0200
@@ -230,10 +230,6 @@
 
 fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial;
 
-(* FIXME unused!? *)
-fun identity_on thy name morph =
-  let val mk_instance = instance_of thy name
-  in ListPair.all Term.aconv_untyped (mk_instance Morphism.identity, mk_instance morph) end;
 
 (* Print instance and qualifiers *)
 
@@ -587,21 +583,6 @@
 
 (*** Dependencies ***)
 
-(* FIXME dead code!?
-fun amend_dependency loc (name, morph) mixin export thy =
-  let
-    val deps = dependencies_of thy loc;
-  in
-    case AList.lookup (fn ((name, morph), ((name', (morph', _)), _)) =>
-      total_ident_ord ((name, instance_of thy name morph), (name', instance_of thy name' morph')) = EQUAL) deps (name, morph) of
-        NONE => error ("Locale " ^
-          quote (extern thy name) ^ " with\parameter instantiation " ^
-          space_implode " " (map (quote o Syntax.string_of_term_global thy) morph) ^
-          " not a sublocale of " ^ quote (extern thy loc))
-      | SOME (_, serial') => change_locale ...
-  end;
-*)
-
 fun add_dependency loc {dep = (name, morph), mixin, export} thy =
   let
     val serial' = serial ();