# HG changeset patch
# User nipkow
# Date 1253207602 -7200
# Node ID 979c274089a504c09ab42e3afa03000721c2c641
# Parent  1e2872252f913ef37281435a82cb2fdcf2128d50# Parent  3a3d2e37fec495123fd3405d130946f7276c50f5
merged

diff -r 3a3d2e37fec4 -r 979c274089a5 Admin/E/eproof
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/E/eproof	Thu Sep 17 19:13:22 2009 +0200
@@ -0,0 +1,92 @@
+#!/usr/bin/perl -w
+#
+# eproof - run E and translate its output into TSTP format
+#
+# Author: Sascha Boehme, TU Muenchen
+#
+# This script is a port of a Bash script with the same name coming with
+# E 1.0-004 (written by Stephan Schulz).
+#
+
+
+use File::Basename qw/ dirname /;
+use File::Temp qw/ tempfile /;
+
+
+# E executables
+
+my $edir = dirname($0);
+my $eprover = "$edir/eprover";
+my $epclextract = "$edir/epclextract";
+
+
+# build E command from given commandline arguments
+
+my $format = "";
+my $timelimit = 2000000000;   # effectively unlimited
+
+my $eprover_cmd = "'$eprover'";
+foreach (@ARGV) {
+  if (m/--cpu-limit=([0-9]+)/) {
+    $timelimit = $1;
+  }
+
+  if (m/--tstp-out/) {
+    $format = $_;
+  }
+  else {
+    $eprover_cmd = "$eprover_cmd '$_'";
+  }
+}
+$eprover_cmd = "$eprover_cmd -l4 -R -o- --pcl-terms-compressed --pcl-compact";
+
+
+# run E, redirecting output into a temporary file
+
+my ($fh, $filename) = tempfile(UNLINK => 1);
+my $r = system "$eprover_cmd > $filename";
+exit ($r >> 8) if $r != 0;
+
+
+# analyze E output
+
+my @lines = <$fh>;
+my $content = join "", @lines[-60 .. -1];
+  # Note: Like the original eproof, we only look at the last 60 lines.
+
+if ($content =~ m/Total time\s*:\s*([0-9]+\.[0-9]+)/) {
+  $timelimit = $timelimit - $1 - 1;
+
+  if ($content =~ m/No proof found!/) {
+    print "# Problem is satisfiable (or invalid), " .
+      "generating saturation derivation\n";
+  }
+  elsif ($content =~ m/Proof found!/) {
+    print "# Problem is unsatisfiable (or provable), " .
+      "constructing proof object\n";
+  }
+  elsif ($content =~ m/Watchlist is empty!/) {
+    print "# All watchlist clauses generated, constructing derivation\n";
+  }
+  else {
+    print "# Cannot determine problem status\n";
+    exit $r;
+  }
+}
+else {
+  print "# Cannot determine problem status within resource limit\n";
+  exit $r;
+}
+
+
+# translate E output
+
+foreach (@lines) {
+  print if (m/# SZS status/ or m/"# Failure"/);
+}
+$r = system ("exec bash -c \"ulimit -S -t $timelimit; " .
+  "'$epclextract' $format -f --competition-framing $filename\"");
+  # Note: Setting the user time is not supported on Cygwin, i.e., ulimit fails
+  # and prints and error message. How could we then limit the execution time?
+exit ($r >> 8);
+
diff -r 3a3d2e37fec4 -r 979c274089a5 NEWS
--- a/NEWS	Thu Sep 17 19:13:07 2009 +0200
+++ b/NEWS	Thu Sep 17 19:13:22 2009 +0200
@@ -41,14 +41,6 @@
 semidefinite programming solvers.  For more information and examples
 see src/HOL/Library/Sum_Of_Squares.
 
-* Set.UNIV and Set.empty are mere abbreviations for top and bot.
-INCOMPATIBILITY.
-
-* More convenient names for set intersection and union.
-INCOMPATIBILITY:
-    Set.Int ~>  Set.inter
-    Set.Un ~>   Set.union
-
 * Code generator attributes follow the usual underscore convention:
     code_unfold     replaces    code unfold
     code_post       replaces    code post
@@ -57,16 +49,14 @@
 
 * New class "boolean_algebra".
 
-* Refinements to lattices classes:
-  - added boolean_algebra type class
+* Refinements to lattice classes and sets:
   - less default intro/elim rules in locale variant, more default
     intro/elim rules in class variant: more uniformity
   - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
   - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
   - renamed ACI to inf_sup_aci
   - class "complete_lattice" moved to separate theory "complete_lattice";
-    corresponding constants renamed:
-    
+    corresponding constants (and abbreviations) renamed:
     Set.Inf ~>      Complete_Lattice.Inf
     Set.Sup ~>      Complete_Lattice.Sup
     Set.INFI ~>     Complete_Lattice.INFI
@@ -75,6 +65,14 @@
     Set.Union ~>    Complete_Lattice.Union
     Set.INTER ~>    Complete_Lattice.INTER
     Set.UNION ~>    Complete_Lattice.UNION
+  - more convenient names for set intersection and union:
+    Set.Int ~>  Set.inter
+    Set.Un ~>   Set.union
+  - mere abbreviations:
+    Set.empty               (for bot)
+    Set.UNIV                (for top)
+    Complete_Lattice.Inter  (for Inf)
+    Complete_Lattice.Union  (for Sup)
 
   INCOMPATIBILITY.
 
@@ -87,7 +85,7 @@
 INCOMPATIBILITY.
 
 * Power operations on relations and functions are now one dedicate
-constant compow with infix syntax "^^".  Power operations on
+constant "compow" with infix syntax "^^".  Power operations on
 multiplicative monoids retains syntax "^" and is now defined generic
 in class power.  INCOMPATIBILITY.
 
@@ -129,6 +127,9 @@
 ATPs down considerably but eliminates a source of unsound "proofs"
 that fail later.
 
+* New method metisFT: A version of metis that uses full type information
+in order to avoid failures of proof reconstruction.
+
 * Discontinued ancient tradition to suffix certain ML module names
 with "_package", e.g.:
 
diff -r 3a3d2e37fec4 -r 979c274089a5 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy	Thu Sep 17 19:13:22 2009 +0200
@@ -203,8 +203,8 @@
 
 subsection {* Union *}
 
-definition Union :: "'a set set \<Rightarrow> 'a set" where
-  Sup_set_eq [symmetric]: "Union S = \<Squnion>S"
+abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
+  "Union S \<equiv> \<Squnion>S"
 
 notation (xsymbols)
   Union  ("\<Union>_" [90] 90)
@@ -216,7 +216,7 @@
   have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
     by auto
   then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
-    by (simp add: Sup_set_eq [symmetric] Sup_fun_def Sup_bool_def) (simp add: mem_def)
+    by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
 qed
 
 lemma Union_iff [simp, noatp]:
@@ -314,7 +314,7 @@
 
 lemma UNION_eq_Union_image:
   "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
-  by (simp add: SUPR_def SUPR_set_eq [symmetric] Sup_set_eq)
+  by (simp add: SUPR_def SUPR_set_eq [symmetric])
 
 lemma Union_def:
   "\<Union>S = (\<Union>x\<in>S. x)"
@@ -439,8 +439,8 @@
 
 subsection {* Inter *}
 
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
-  Inf_set_eq [symmetric]: "Inter S = \<Sqinter>S"
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
+  "Inter S \<equiv> \<Sqinter>S"
   
 notation (xsymbols)
   Inter  ("\<Inter>_" [90] 90)
@@ -452,7 +452,7 @@
   have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
     by auto
   then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
-    by (simp add: Inf_fun_def Inf_bool_def Inf_set_eq [symmetric]) (simp add: mem_def)
+    by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
 qed
 
 lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
@@ -541,7 +541,7 @@
 
 lemma INTER_eq_Inter_image:
   "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
-  by (simp add: INFI_def INFI_set_eq [symmetric] Inf_set_eq)
+  by (simp add: INFI_def INFI_set_eq [symmetric])
   
 lemma Inter_def:
   "\<Inter>S = (\<Inter>x\<in>S. x)"
diff -r 3a3d2e37fec4 -r 979c274089a5 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/Inductive.thy	Thu Sep 17 19:13:22 2009 +0200
@@ -111,8 +111,7 @@
   and P_f: "!!S. P S ==> P(f S)"
   and P_Union: "!!M. !S:M. P S ==> P(Union M)"
   shows "P(lfp f)"
-  using assms unfolding Sup_set_eq [symmetric]
-  by (rule lfp_ordinal_induct [where P=P])
+  using assms by (rule lfp_ordinal_induct [where P=P])
 
 
 text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 
diff -r 3a3d2e37fec4 -r 979c274089a5 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Thu Sep 17 19:13:22 2009 +0200
@@ -8,7 +8,7 @@
 imports Main Fset
 begin
 
-subsection {* Derived set operations *}
+subsection {* Preprocessor setup *}
 
 declare member [code] 
 
@@ -24,9 +24,7 @@
 definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   [code del]: "eq_set = op ="
 
-(* FIXME allow for Stefan's code generator:
-declare set_eq_subset[code_unfold]
-*)
+(*declare eq_set_def [symmetric, code_unfold]*)
 
 lemma [code]:
   "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
@@ -37,13 +35,20 @@
 declare Inter_image_eq [symmetric, code]
 declare Union_image_eq [symmetric, code]
 
-
-subsection {* Rewrites for primitive operations *}
-
 declare List_Set.project_def [symmetric, code_unfold]
 
+definition Inter :: "'a set set \<Rightarrow> 'a set" where
+  "Inter = Complete_Lattice.Inter"
 
-subsection {* code generator setup *}
+declare Inter_def [symmetric, code_unfold]
+
+definition Union :: "'a set set \<Rightarrow> 'a set" where
+  "Union = Complete_Lattice.Union"
+
+declare Union_def [symmetric, code_unfold]
+
+
+subsection {* Code generator setup *}
 
 ML {*
 nonfix inter;
@@ -75,8 +80,8 @@
   "op \<union>"              ("{*Fset.union*}")
   "op \<inter>"              ("{*Fset.inter*}")
   "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
-  "Complete_Lattice.Union" ("{*Fset.Union*}")
-  "Complete_Lattice.Inter" ("{*Fset.Inter*}")
+  "Union"             ("{*Fset.Union*}")
+  "Inter"             ("{*Fset.Inter*}")
   card                ("{*Fset.card*}")
   fold                ("{*foldl o flip*}")
 
diff -r 3a3d2e37fec4 -r 979c274089a5 src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Thu Sep 17 19:13:22 2009 +0200
@@ -11134,7 +11134,6 @@
   shows "pi1\<bullet>(lfp f) = lfp (pi1\<bullet>f)"
   and   "pi2\<bullet>(lfp g) = lfp (pi2\<bullet>g)"
 apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
 apply(simp add: big_inter_eqvt)
 apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
 apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
@@ -11146,7 +11145,6 @@
 apply(drule subseteq_eqvt(1)[THEN iffD2])
 apply(simp add: perm_bool)
 apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
 apply(simp add: big_inter_eqvt)
 apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
 apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
diff -r 3a3d2e37fec4 -r 979c274089a5 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/SetInterval.thy	Thu Sep 17 19:13:22 2009 +0200
@@ -514,6 +514,30 @@
 qed
 
 
+subsubsection {* Proving Inclusions and Equalities between Unions *}
+
+lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
+  by (auto simp add: atLeast0LessThan) 
+
+lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
+  by (subst UN_UN_finite_eq [symmetric]) blast
+
+lemma UN_finite2_subset:
+  assumes sb: "!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)"
+  shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
+proof (rule UN_finite_subset)
+  fix n
+  have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)" by (rule sb)
+  also have "...  \<subseteq> (\<Union>n::nat. \<Union>i\<in>{0..<n}. B i)" by blast
+  also have "... = (\<Union>n. B n)" by (simp add: UN_UN_finite_eq) 
+  finally show "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>n. B n)" .
+qed
+
+lemma UN_finite2_eq:
+  "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)"
+  by (iprover intro: subset_antisym UN_finite2_subset elim: equalityE)  
+
+
 subsubsection {* Cardinality *}
 
 lemma card_lessThan [simp]: "card {..<u} = u"
diff -r 3a3d2e37fec4 -r 979c274089a5 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Sep 17 19:13:22 2009 +0200
@@ -79,14 +79,17 @@
       preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
 
     (* write out problem file and call prover *)
-    val perl_script = "perl -w $ISABELLE_ATP_MANAGER/lib/scripts/local_atp.pl"
-    fun cmd_line probfile = perl_script ^ " '" ^ space_implode " "
-      [File.shell_path cmd, args, File.platform_path probfile] ^ "'"
+    fun cmd_line probfile = "TIMEFORMAT='%3U'; { time " ^ space_implode " "
+      [File.shell_path cmd, args, File.platform_path probfile] ^ " ; } 2>&1"
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n")
         val (proof, t) = s |> split |> split_last |> apfst cat_lines
-        val time = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
+        fun as_num f = f >> (fst o read_int)
+        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
+        val digit = Scan.one Symbol.is_ascii_digit
+        val num3 = as_num (digit ::: digit ::: (digit >> single))
+        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode
       in (proof, as_time t) end
     fun run_on probfile =
@@ -97,7 +100,7 @@
       else error ("Bad executable: " ^ Path.implode cmd)
 
     (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
-    fun cleanup probfile = if destdir' = "" then File.rm probfile else ()
+    fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE
     fun export probfile (((proof, _), _), _) = if destdir' = "" then ()
       else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
 
diff -r 3a3d2e37fec4 -r 979c274089a5 src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl
--- a/src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl	Thu Sep 17 19:13:07 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-use POSIX qw(setsid);
-
-$SIG{'INT'} = "DEFAULT";
-
-defined (my $pid = fork) or die "$!";
-if (not $pid) {
-  POSIX::setsid or die $!;
-  exec @ARGV;
-}
-else {
-  wait;
-  my ($user, $system, $cuser, $csystem) = times;
-  my $time = ($user + $cuser) * 1000;
-  print "$time\n";
-}
diff -r 3a3d2e37fec4 -r 979c274089a5 src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Thu Sep 17 19:13:22 2009 +0200
@@ -88,7 +88,7 @@
 done
 
 lemma wens_Id [simp]: "wens F Id B = B"
-by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def, blast)
 
 text{*These two theorems justify the claim that @{term wens} returns the
 weakest assertion satisfying the ensures property*}
@@ -101,7 +101,7 @@
 
 lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
 by (simp add: wens_def gfp_def constrains_def awp_def wp_def
-              ensures_def transient_def Sup_set_eq, blast)
+              ensures_def transient_def, blast)
 
 text{*These two results constitute assertion (4.13) of the thesis*}
 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
 done
 
 lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def, blast)
 
 text{*Assertion (6), or 4.16 in the thesis*}
 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
@@ -120,7 +120,7 @@
 
 text{*Assertion 4.17 in the thesis*}
 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
   --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
       is declared as an iff-rule, then it's almost impossible to prove. 
       One proof is via @{text meson} after expanding all definitions, but it's
@@ -331,7 +331,7 @@
 
 lemma wens_single_eq:
      "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def, blast)
 
 
 text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
diff -r 3a3d2e37fec4 -r 979c274089a5 src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/ex/CTL.thy	Thu Sep 17 19:13:22 2009 +0200
@@ -95,7 +95,7 @@
     proof
       assume "x \<in> gfp (\<lambda>s. - f (- s))"
       then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
-	by (auto simp add: gfp_def Sup_set_eq)
+        by (auto simp add: gfp_def)
       then have "f (- u) \<subseteq> - u" by auto
       then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
       from l and this have "x \<notin> u" by auto
diff -r 3a3d2e37fec4 -r 979c274089a5 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Sep 17 19:13:22 2009 +0200
@@ -84,7 +84,7 @@
 fun group_of (Future {group, ...}) = group;
 fun result_of (Future {result, ...}) = result;
 
-fun peek x = Synchronized.peek (result_of x);
+fun peek x = Synchronized.value (result_of x);
 fun is_finished x = is_some (peek x);
 
 fun value x = Future
diff -r 3a3d2e37fec4 -r 979c274089a5 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Thu Sep 17 19:13:22 2009 +0200
@@ -8,7 +8,6 @@
 sig
   type 'a var
   val var: string -> 'a -> 'a var
-  val peek: 'a var -> 'a
   val value: 'a var -> 'a
   val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
   val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
@@ -33,9 +32,7 @@
   cond = ConditionVar.conditionVar (),
   var = ref x};
 
-fun peek (Var {var, ...}) = ! var;  (*unsynchronized!*)
-
-fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var);
+fun value (Var {var, ...}) = ! var;
 
 
 (* synchronized access *)
diff -r 3a3d2e37fec4 -r 979c274089a5 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/Pure/General/binding.ML	Thu Sep 17 19:13:22 2009 +0200
@@ -30,18 +30,19 @@
   val str_of: binding -> string
 end;
 
-structure Binding:> BINDING =
+structure Binding: BINDING =
 struct
 
 (** representation **)
 
 (* datatype *)
 
-datatype binding = Binding of
+abstype binding = Binding of
  {prefix: (string * bool) list,     (*system prefix*)
   qualifier: (string * bool) list,  (*user qualifier*)
   name: bstring,                    (*base name*)
-  pos: Position.T};                 (*source position*)
+  pos: Position.T}                  (*source position*)
+with
 
 fun make_binding (prefix, qualifier, name, pos) =
   Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
@@ -109,6 +110,7 @@
   in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
 
 end;
+end;
 
 type binding = Binding.binding;
 
diff -r 3a3d2e37fec4 -r 979c274089a5 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/Pure/General/linear_set.scala	Thu Sep 17 19:13:22 2009 +0200
@@ -93,11 +93,11 @@
     }
 
   def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
-    (elems :\ this)((elem: A, ls: Linear_Set[A]) => ls.insert_after(hook, elem))
+    (elems :\ this)((elem, set) => set.insert_after(hook, elem))
 
   def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
   {
-    if (!rep.first.isDefined) this
+    if (isEmpty) this
     else {
       val next =
         if (from == rep.last) None
@@ -123,7 +123,7 @@
     def hasNext = next_elem.isDefined
     def next = {
       val elem = next_elem.get
-      next_elem = if (rep.nexts.isDefinedAt(elem)) Some(rep.nexts(elem)) else None
+      next_elem = rep.nexts.get(elem)
       elem
     }
   }
diff -r 3a3d2e37fec4 -r 979c274089a5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Sep 17 19:13:07 2009 +0200
+++ b/src/Pure/thm.ML	Thu Sep 17 19:13:22 2009 +0200
@@ -153,7 +153,7 @@
   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
 
-structure Thm:> THM =
+structure Thm: THM =
 struct
 
 structure Pt = Proofterm;
@@ -163,11 +163,12 @@
 
 (** certified types **)
 
-datatype ctyp = Ctyp of
+abstype ctyp = Ctyp of
  {thy_ref: theory_ref,
   T: typ,
   maxidx: int,
-  sorts: sort OrdList.T};
+  sorts: sort OrdList.T}
+with
 
 fun rep_ctyp (Ctyp args) = args;
 fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
@@ -189,12 +190,13 @@
 (** certified terms **)
 
 (*certified terms with checked typ, maxidx, and sorts*)
-datatype cterm = Cterm of
+abstype cterm = Cterm of
  {thy_ref: theory_ref,
   t: term,
   T: typ,
   maxidx: int,
-  sorts: sort OrdList.T};
+  sorts: sort OrdList.T}
+with
 
 exception CTERM of string * cterm list;
 
@@ -337,7 +339,7 @@
 
 (*** Derivations and Theorems ***)
 
-datatype thm = Thm of
+abstype thm = Thm of
  deriv *                                        (*derivation*)
  {thy_ref: theory_ref,                          (*dynamic reference to theory*)
   tags: Properties.T,                           (*additional annotations/comments*)
@@ -348,7 +350,8 @@
   prop: term}                                   (*conclusion*)
 and deriv = Deriv of
  {promises: (serial * thm future) OrdList.T,
-  body: Pt.proof_body};
+  body: Pt.proof_body}
+with
 
 type conv = cterm -> thm;
 
@@ -1718,6 +1721,10 @@
       end
   end;
 
+end;
+end;
+end;
+
 
 (* authentic derivation names *)