# HG changeset patch
# User ballarin
# Date 1257798802 -3600
# Node ID e716c6ad381b22dcf659a54eaf7bb68391ff2230
# Parent  b233f48a4d3d8865a79fc813d0ceebc7f9a51427
Removed obsolete code.

diff -r b233f48a4d3d -r e716c6ad381b src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Nov 09 16:06:08 2009 +0000
+++ b/src/Pure/Isar/locale.ML	Mon Nov 09 21:33:22 2009 +0100
@@ -72,8 +72,6 @@
     morphism -> theory -> theory
   val amend_registration: string * morphism -> morphism * bool ->
     morphism -> theory -> theory
-  val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
-  val amend_registration_legacy: morphism -> string * morphism -> theory -> theory
   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
 
   (* Diagnostic *)
@@ -239,7 +237,7 @@
 
 in
 
-(* Note that while identifiers always have the external (exported) view, activate_dep is
+(* Note that while identifiers always have the external (exported) view, activate_dep
   is presented with the internal view. *)
 
 fun roundup thy activate_dep export (name, morph) (marked, input) =
@@ -481,36 +479,6 @@
       end
   end;
 
-fun amend_registration_legacy morph (name, base_morph) thy =
-  (* legacy, never modify base morphism *)
-  let
-    val regs = Registrations.get thy |> fst |> map fst;
-    val base = instance_of thy name base_morph;
-    fun match (name', (morph', _)) =
-      name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
-    val i = find_index match (rev regs);
-    val _ =
-      if i = ~1 then error ("No registration of locale " ^
-        quote (extern thy name) ^ " and parameter instantiation " ^
-        space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
-      else ();
-  in
-    Registrations.map ((apfst o nth_map (length regs - 1 - i))
-      (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
-  end;
-
-fun add_registration_eqs (dep, proto_morph) eqns export thy =
-  let
-    val morph = if null eqns then proto_morph
-      else proto_morph $> Element.eq_morphism thy eqns;
-  in
-    (get_idents (Context.Theory thy), thy)
-    |> roundup thy (fn (dep', morph') =>
-        Registrations.map (apfst (cons ((dep', (morph', export)), stamp ())))) export (dep, morph)
-    |> snd
-    |> Context.theory_map (activate_facts (dep, morph $> export))
-  end;
-
 
 (*** Dependencies ***)