--- 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 *)