# HG changeset patch
# User haftmann
# Date 1187351937 -7200
# Node ID 32b67bdf2c3aaea93c2b7c84e347021ff82ce298
# Parent  3045683749af877d163a63e731e150dfa56e54c5
dropped junk

diff -r 3045683749af -r 32b67bdf2c3a src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Aug 17 09:20:45 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Aug 17 13:58:57 2007 +0200
@@ -2424,7 +2424,6 @@
   have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
     using insert
-    thm ACIf.fold1_insert_idem_def
  by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def])
   also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
   also have "\<dots> = \<Sqinter>{x \<squnion> b|b. b \<in> B} \<sqinter> \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
diff -r 3045683749af -r 32b67bdf2c3a src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Aug 17 09:20:45 2007 +0200
+++ b/src/HOL/Set.thy	Fri Aug 17 13:58:57 2007 +0200
@@ -147,7 +147,6 @@
 instance set :: (type) ord
   subset_def:  "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
   psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
-
 lemmas [code func del] = subset_def psubset_def
 
 abbreviation
diff -r 3045683749af -r 32b67bdf2c3a src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Fri Aug 17 09:20:45 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Fri Aug 17 13:58:57 2007 +0200
@@ -163,7 +163,7 @@
 
 in
 
-fun defs loc kind args lthy0 =
+fun defs kind args lthy0 =
   let
     fun def ((c, mx), ((name, atts), rhs)) lthy1 =
       let
@@ -350,7 +350,7 @@
       consts = consts is_loc some_class,
       axioms = axioms,
       abbrev = abbrev is_loc some_class,
-      defs = defs loc,
+      defs = defs,
       notes = notes loc,
       type_syntax = type_syntax loc,
       term_syntax = term_syntax loc,