Remove garbage.
authorballarin
Tue Apr 20 22:34:17 2010 +0200 (2010-04-20)
changeset 3624095a3fac5dcae
parent 36239 1385c4172d47
child 36241 2a4cec6bcae2
Remove garbage.
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Apr 20 22:31:08 2010 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Apr 20 22:34:17 2010 +0200
     1.3 @@ -142,13 +142,8 @@
     1.4    thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
     1.5      (binding,
     1.6        mk_locale ((parameters, spec, intros, axioms),
     1.7 -(* <<<<<<< local
     1.8 -        ((pairself (map (fn decl => (decl, serial ()))) decls, map (fn n => (n, serial ())) notes),
     1.9 -          map (fn d => (d, serial ())) dependencies))) #> snd);
    1.10 -======= *)
    1.11          ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
    1.12            map (fn d => (d, serial ())) dependencies))) #> snd);
    1.13 -(* >>>>>>> other *)
    1.14  
    1.15  fun change_locale name =
    1.16    Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
    1.17 @@ -521,16 +516,7 @@
    1.18  
    1.19  (* Declarations *)
    1.20  
    1.21 -(* <<<<<<< local
    1.22 -local
    1.23 -
    1.24 -fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
    1.25 -
    1.26 -fun add_decls add loc decl =
    1.27 -  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, serial ()))) #>
    1.28 -======= *)
    1.29  fun add_declaration loc decl =
    1.30 -(* >>>>>>> other *)
    1.31    add_thmss loc ""
    1.32      [((Binding.conceal Binding.empty,
    1.33          [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),