diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/Ctr_Sugar/local_interpretation.ML
--- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Mon Oct 13 17:04:25 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(*  Title:      HOL/Tools/Ctr_Sugar/local_interpretation.ML
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Generic interpretation of local theory data -- ad hoc. Based on
-
-    Title:      Pure/interpretation.ML
-    Author:     Florian Haftmann and Makarius
-*)
-
-signature LOCAL_INTERPRETATION =
-sig
-  type T
-  val result: theory -> T list
-  val interpretation: string -> (T -> theory -> theory) -> (T -> local_theory -> local_theory) ->
-    theory -> theory
-  val data: (string -> bool) -> T -> local_theory -> local_theory
-  val data_global: (string -> bool) -> T -> theory -> theory
-  val init: theory -> theory
-end;
-
-functor Local_Interpretation(type T val eq: T * T -> bool): LOCAL_INTERPRETATION =
-struct
-
-type T = T;
-
-structure Interp = Theory_Data
-(
-  type T =
-    ((Name_Space.naming * (string -> bool)) * T) list
-    * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * (string * stamp))
-       * ((Name_Space.naming * (string -> bool)) * T) list) list;
-  val empty = ([], []);
-  val extend = I;
-  fun merge ((data1, interps1), (data2, interps2)) : T =
-    (Library.merge (eq_snd eq) (data1, data2),
-     AList.join (eq_snd (op =)) (K (Library.merge (eq_snd eq))) (interps1, interps2));
-);
-
-val result = map snd o fst o Interp.get;
-
-fun consolidate_common g_or_f lift_lthy thy thy_or_lthy =
-  let
-    val (data, interps) = Interp.get thy;
-
-    fun unfinished_of ((gf, (name, _)), data') =
-      (g_or_f gf,
-       if eq_list (eq_snd eq) (data', data) then
-         []
-       else
-         subtract (eq_snd eq) data' data
-         |> map_filter (fn ((naming, keep), x) => if keep name then SOME (naming, x) else NONE));
-
-    val unfinished = map unfinished_of interps;
-    val finished = map (apsnd (K data)) interps;
-  in
-    if forall (null o #2) unfinished then
-      NONE
-    else
-      SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished
-        |> lift_lthy (Interp.put (data, finished)))
-  end;
-
-fun consolidate lthy =
-  consolidate_common (fn (_, g) => fn (_, x) => g x) Local_Theory.background_theory
-    (Proof_Context.theory_of lthy) lthy;
-
-fun consolidate_global thy =
-  consolidate_common (fn (f, _) => fn (naming, x) => fn thy =>
-    thy |> Sign.map_naming (K naming) |> f x |> Sign.restore_naming thy) I thy thy;
-
-fun interpretation name g f =
-  Interp.map (apsnd (cons (((g, f), (name, stamp ())), []))) #> perhaps consolidate_global;
-
-fun data keep x =
-  Local_Theory.background_theory
-    (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
-  #> perhaps consolidate;
-
-fun data_global keep x =
-  (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
-  #> perhaps consolidate_global;
-
-val init = Theory.at_begin consolidate_global;
-
-end;