# HG changeset patch
# User ballarin
# Date 1271795657 -7200
# Node ID 95a3fac5dcaeedacb5dfe27b8ab173e9f4de2d88
# Parent  1385c4172d47d0b602051c398fdcdb9e9c264c80
Remove garbage.

diff -r 1385c4172d47 -r 95a3fac5dcae src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Apr 20 22:31:08 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Apr 20 22:34:17 2010 +0200
@@ -142,13 +142,8 @@
   thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
     (binding,
       mk_locale ((parameters, spec, intros, axioms),
-(* <<<<<<< local
-        ((pairself (map (fn decl => (decl, serial ()))) decls, map (fn n => (n, serial ())) notes),
-          map (fn d => (d, serial ())) dependencies))) #> snd);
-======= *)
         ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
           map (fn d => (d, serial ())) dependencies))) #> snd);
-(* >>>>>>> other *)
 
 fun change_locale name =
   Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
@@ -521,16 +516,7 @@
 
 (* Declarations *)
 
-(* <<<<<<< local
-local
-
-fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
-
-fun add_decls add loc decl =
-  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, serial ()))) #>
-======= *)
 fun add_declaration loc decl =
-(* >>>>>>> other *)
   add_thmss loc ""
     [((Binding.conceal Binding.empty,
         [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),