# HG changeset patch
# User ballarin
# Date 1271795468 -7200
# Node ID 1385c4172d47d0b602051c398fdcdb9e9c264c80
# Parent  344377ce2e0a2a3f447e649b36bf4783212f0c43
Remove garbage.

diff -r 344377ce2e0a -r 1385c4172d47 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Apr 20 17:07:53 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Apr 20 22:31:08 2010 +0200
@@ -95,15 +95,9 @@
   intros: thm option * thm option,
   axioms: thm list,
   (** dynamic part **)
-(* <<<<<<< local
-  decls: (declaration * serial) list * (declaration * serial) list,
-    (* type and term syntax declarations *)
-  notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
-======= *)
   syntax_decls: (declaration * serial) list,
     (* syntax declarations *)
   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
-(* >>>>>>> other *)
     (* theorem declarations *)
   dependencies: ((string * morphism) * serial) list
     (* locale dependencies (sublocale relation) *)