# HG changeset patch
# User huffman
# Date 1266860616 28800
# Node ID 978a936faace2d3cc5081ce629df40faa53e1f08
# Parent  0e5fe22fa321523433949d64f8a693d57d34264a
remove unnecessary local

diff -r 0e5fe22fa321 -r 978a936faace src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 21 08:59:39 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 22 09:43:36 2010 -0800
@@ -24,8 +24,6 @@
 fun message s = if !quiet_mode then () else writeln s;
 fun trace s = if !trace_domain then tracing s else ();
 
-local
-
 val adm_impl_admw = @{thm adm_impl_admw};
 val adm_all = @{thm adm_all};
 val adm_conj = @{thm adm_conj};
@@ -134,8 +132,6 @@
 
 val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)}
 
-in
-
 fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
 let
 
@@ -1089,5 +1085,4 @@
            else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
        |> Sign.parent_path |> pair take_rews
 end; (* let *)
-end; (* local *)
 end; (* struct *)