# HG changeset patch
# User haftmann
# Date 1170141677 -3600
# Node ID 86b688409ddef736e57a3ceee8d8defd9fce541e
# Parent  2d6e8cf4867095e5a742e1fce18bd61dc792bf75
dropped dead code

diff -r 2d6e8cf48670 -r 86b688409dde src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Tue Jan 30 08:21:16 2007 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Jan 30 08:21:17 2007 +0100
@@ -467,25 +467,6 @@
       |> map (NameSpace.base o fst o fst) (*FIXME*)
     fun mk_const thy class (c, ty) =
       Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty);
-    (*fun note_thms class name_locale cs thy =
-      let (*FIXME just an ad-hoc feature*)
-        val names = fold (fn Element.Assumes xs => fold (cons o fst o fst) xs
-          | Element.Notes (name, _) => cons name
-          | _ => I) elems []
-        val const_names = cs;
-        val path = NameSpace.base class;
-        val prefix = NameSpace.implode [class ^ "_class", space_implode "_" const_names];
-        fun note_thm name thy =
-          case try (PureThy.get_thm thy) (Name (NameSpace.append prefix name))
-           of SOME thm =>
-                thy
-                |> PureThy.note_thmss_qualified "" path [((name, []), [([thm], [])])]
-                |> snd
-            | NONE => error name;
-      in
-        thy
-        |> fold note_thm names
-      end;*)
   in
     thy
     |> add_locale bname supexpr elems
@@ -502,7 +483,6 @@
       #> prove_interpretation (Logic.const_of_class bname, [])
           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts))
             ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
-      (*#> note_thms name_axclass name_locale (map fst supconsts @ map (fst o fst) params)*)
       #> pair name_axclass
       )))))
   end;