# HG changeset patch
# User wenzelm
# Date 1377726525 -7200
# Node ID 082d0972096bb8b9c922b111fc889d739e9fbc15
# Parent  16235bb41881acea808e8234eff23daff634d4b7# Parent  220f306f5c4ead7792efcaeda423d1b2762a58d4
merged

diff -r 220f306f5c4e -r 082d0972096b etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Aug 28 23:41:21 2013 +0200
+++ b/etc/isar-keywords.el	Wed Aug 28 23:48:45 2013 +0200
@@ -195,10 +195,10 @@
     "print_methods"
     "print_options"
     "print_orders"
+    "print_quot_maps"
     "print_quotconsts"
     "print_quotients"
     "print_quotientsQ3"
-    "print_quotmaps"
     "print_quotmapsQ3"
     "print_rules"
     "print_simpset"
@@ -422,10 +422,10 @@
     "print_methods"
     "print_options"
     "print_orders"
+    "print_quot_maps"
     "print_quotconsts"
     "print_quotients"
     "print_quotientsQ3"
-    "print_quotmaps"
     "print_quotmapsQ3"
     "print_rules"
     "print_simpset"
diff -r 220f306f5c4e -r 082d0972096b src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -1550,7 +1550,7 @@
   \begin{matharray}{rcl}
     @{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
     @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
-    @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
+    @{command_def (HOL) "print_quot_maps"} & : & @{text "context \<rightarrow>"}\\
     @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
     @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
     @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
@@ -1626,7 +1626,7 @@
     Integration with code: For total quotients, @{command
     (HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation.
 
-  \item @{command (HOL) "print_quotmaps"} prints stored quotient map
+  \item @{command (HOL) "print_quot_maps"} prints stored quotient map
     theorems.
 
   \item @{command (HOL) "print_quotients"} prints stored quotient
diff -r 220f306f5c4e -r 082d0972096b src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Aug 28 23:48:45 2013 +0200
@@ -601,14 +601,15 @@
 \point{A strange error occurred---what should I do?}
 
 Sledgehammer tries to give informative error messages. Please report any strange
-error to the author at \authoremail. This applies double if you get the message
+error to the author at \authoremail. This applies doubly if you get the message
 
 \prew
 \slshape
-The prover found a type-unsound proof involving ``\textit{foo\/}'',
-``\textit{bar\/}'', and ``\textit{baz\/}'' even though a supposedly type-sound
-encoding was used (or, less likely, your axioms are inconsistent). You might
-want to report this to the Isabelle developers.
+The prover derived ``\textit{False}'' using ``\textit{foo\/}'',
+``\textit{bar\/}'', and ``\textit{baz\/}''.
+This could be due to inconsistent axioms (including ``\textbf{sorry}''s) or to
+a bug in Sledgehammer. If the problem persists, please contact the
+Isabelle developers.
 \postw
 
 \point{Auto can solve it---why not Sledgehammer?}
diff -r 220f306f5c4e -r 082d0972096b src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Aug 28 23:48:45 2013 +0200
@@ -14,8 +14,11 @@
   type unfold_set
   val empty_unfolds: unfold_set
 
+  exception BAD_DEAD of typ * typ
+
   val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
-    ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
+    ((string * sort) list list -> (string * sort) list) -> (string * sort) list -> typ ->
+    unfold_set * Proof.context ->
     (BNF_Def.bnf * (typ list * typ list)) * (unfold_set * Proof.context)
   val default_comp_sort: (string * sort) list list -> (string * sort) list
   val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
@@ -645,10 +648,18 @@
     ((bnf', deads), lthy')
   end;
 
-fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
-  | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
-  | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold_set, lthy) =
+exception BAD_DEAD of typ * typ;
+
+fun bnf_of_typ _ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
+  | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
+  | bnf_of_typ const_policy qualify' sort Xs (T as Type (C, Ts)) (unfold_set, lthy) =
     let
+      fun check_bad_dead ((_, (deads, _)), _) =
+        let val Ds = fold Term.add_tfreesT deads [] in
+          (case Library.inter (op =) Ds Xs of [] => ()
+           | X :: _ => raise BAD_DEAD (TFree X, T))
+        end;
+
       val tfrees = Term.add_tfreesT T [];
       val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
     in
@@ -679,11 +690,12 @@
             val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
             val ((inners, (Dss, Ass)), (unfold_set', lthy')) =
               apfst (apsnd split_list o split_list)
-                (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort)
+                (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort Xs)
                 (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy));
           in
             compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy')
           end)
+      |> tap check_bad_dead
     end;
 
 end;
diff -r 220f306f5c4e -r 082d0972096b src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 28 23:48:45 2013 +0200
@@ -97,6 +97,7 @@
 
 open BNF_Util
 open BNF_Ctr_Sugar
+open BNF_Comp
 open BNF_Def
 open BNF_FP_Util
 open BNF_FP_Def_Sugar_Tactics
@@ -1103,12 +1104,14 @@
           quote (Syntax.string_of_typ fake_lthy T)))
       | eq_fpT_check _ _ = false;
 
-    fun freeze_fp (T as Type (s, Us)) =
+    fun freeze_fp (T as Type (s, Ts)) =
         (case find_index (eq_fpT_check T) fake_Ts of
-          ~1 => Type (s, map freeze_fp Us)
+          ~1 => Type (s, map freeze_fp Ts)
         | kk => nth Xs kk)
       | freeze_fp T = T;
 
+    val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts);
+
     val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss;
     val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
 
@@ -1120,7 +1123,33 @@
            dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...},
            lthy)) =
       fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
-        no_defs_lthy0;
+        no_defs_lthy0
+      handle BAD_DEAD (X, X_backdrop) =>
+        (case X_backdrop of
+          Type (bad_tc, _) =>
+          let
+            val qsoty = quote o Syntax.string_of_typ fake_lthy;
+            val fake_T = qsoty (unfreeze_fp X);
+            val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop);
+            fun register_hint () =
+              "\nUse the " ^ quote (fst (fst @{command_spec "bnf"})) ^ " command to register " ^
+              quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
+              \it";
+          in
+            if is_some (bnf_of no_defs_lthy bad_tc) orelse
+               is_some (fp_sugar_of no_defs_lthy bad_tc) then
+              error ("Non-strictly-positive " ^ co_prefix fp ^ "recursive occurrence of type " ^
+                fake_T ^ " in type expression " ^ fake_T_backdrop)
+            else if is_some (Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy)
+                bad_tc) then
+              error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
+                " via the old-style datatype " ^ quote bad_tc ^ " in type expression " ^
+                fake_T_backdrop ^ register_hint ())
+            else
+              error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
+                " via type constructor " ^ quote bad_tc ^ " in type expression " ^ fake_T_backdrop ^
+                register_hint ())
+          end);
 
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
diff -r 220f306f5c4e -r 082d0972096b src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Wed Aug 28 23:48:45 2013 +0200
@@ -352,7 +352,7 @@
 fun co_prefix fp = (if fp = Greatest_FP then "co" else "");
 
 fun add_components_of_typ (Type (s, Ts)) =
-    fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
+    cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts
   | add_components_of_typ _ = I;
 
 fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
@@ -571,18 +571,18 @@
     |> unfold_thms ctxt unfolds
   end;
 
-fun fp_bnf construct_fp bs resBs eqs lthy =
+fun fp_bnf construct_fp bs resBs fp_eqs lthy =
   let
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
-    val (lhss, rhss) = split_list eqs;
+    val (Xs, rhsXs) = split_list fp_eqs;
 
-    (* FIXME: because of "@ lhss", the output could contain type variables that are not in the
+    (* FIXME: because of "@ Xs", the output could contain type variables that are not in the
        input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
     fun fp_sort Ass =
-      subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ lhss;
+      subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
 
-    val name = mk_common_name (map Binding.name_of bs);
+    val common_name = mk_common_name (map Binding.name_of bs);
 
     fun raw_qualify b =
       let val s = Binding.name_of b in
@@ -590,21 +590,17 @@
       end;
 
     val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list)
-      (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort) bs rhss
+      (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs) bs rhsXs
         (empty_unfolds, lthy));
 
     fun qualify i =
-      let val namei = name ^ nonzero_string_of_int i;
+      let val namei = common_name ^ nonzero_string_of_int i;
       in Binding.qualify true namei end;
 
     val Ass = map (map dest_TFree) livess;
     val resDs = fold (subtract (op =)) Ass resBs;
     val Ds = fold (fold Term.add_tfreesT) deadss [];
 
-    val _ = (case Library.inter (op =) Ds lhss of [] => ()
-      | A :: _ => error ("Inadmissible type recursion (cannot take fixed point of dead type \
-        \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
-
     val timer = time (timer "Construction of BNFs");
 
     val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) =
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -246,7 +246,7 @@
 
 end
 
-class linear_continuum = conditionally_complete_linorder + inner_dense_linorder +
+class linear_continuum = conditionally_complete_linorder + dense_linorder +
   assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"
 begin
 
@@ -283,22 +283,22 @@
 lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
   using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
 
-lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
+lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
   by (auto intro!: cSup_eq_non_empty intro: dense_le)
 
-lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
+lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
   by (auto intro!: cSup_eq intro: dense_le_bounded)
 
-lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
+lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
   by (auto intro!: cSup_eq intro: dense_le_bounded)
 
-lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, dense_linorder} <..} = x"
+lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, unbounded_dense_linorder} <..} = x"
   by (auto intro!: cInf_eq intro: dense_ge)
 
-lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
+lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
   by (auto intro!: cInf_eq intro: dense_ge_bounded)
 
-lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
+lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
   by (auto intro!: cInf_eq intro: dense_ge_bounded)
 
 end
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -243,7 +243,7 @@
 
 section {* The classical QE after Langford for dense linear orders *}
 
-context dense_linorder
+context unbounded_dense_linorder
 begin
 
 lemma interval_empty_iff: "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
@@ -299,7 +299,8 @@
 lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq 
   le_less neq_iff linear less_not_permute
 
-lemma axiom[no_atp]: "class.dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
+lemma axiom[no_atp]: "class.unbounded_dense_linorder (op \<le>) (op <)"
+  by (rule unbounded_dense_linorder_axioms)
 lemma atoms[no_atp]:
   shows "TERM (less :: 'a \<Rightarrow> _)"
     and "TERM (less_eq :: 'a \<Rightarrow> _)"
@@ -452,7 +453,7 @@
   assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
     and between_same: "between x x = x"
 
-sublocale  constr_dense_linorder < dlo: dense_linorder 
+sublocale  constr_dense_linorder < dlo: unbounded_dense_linorder 
   apply unfold_locales
   using gt_ex lt_ex between_less
   apply auto
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Fields.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -842,7 +842,7 @@
 lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
 by (simp add: field_simps zero_less_two)
 
-subclass dense_linorder
+subclass unbounded_dense_linorder
 proof
   fix x y :: 'a
   from less_add_one show "\<exists>y. x < y" .. 
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -293,7 +293,7 @@
 lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
   using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
 
-instance ereal :: inner_dense_linorder
+instance ereal :: dense_linorder
   by default (blast dest: ereal_dense2)
 
 instance ereal :: ordered_ab_semigroup_add
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Library/Float.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -180,7 +180,7 @@
     and real_of_float_max: "real (max x y) = max (real x) (real y)"
   by (simp_all add: min_def max_def)
 
-instance float :: dense_linorder
+instance float :: unbounded_dense_linorder
 proof
   fix a b :: float
   show "\<exists>c. a < c"
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -9,13 +9,13 @@
 begin
 
 lemma le_Sup_iff_less:
-  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+  fixes x :: "'a :: {complete_linorder, dense_linorder}"
   shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
   unfolding le_SUP_iff
   by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
 
 lemma Inf_le_iff_less:
-  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+  fixes x :: "'a :: {complete_linorder, dense_linorder}"
   shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
   unfolding INF_le_iff
   by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -242,4 +242,55 @@
   shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
 unfolding while_def using assms by (rule lfp_the_while_option) blast
 
+
+text{* Computing the reflexive, transitive closure by iterating a successor
+function. Stops when an element is found that dos not satisfy the test.
+
+More refined (and hence more efficient) versions can be found in ITP 2011 paper
+by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow)
+and the AFP article Executable Transitive Closures by René Thiemann. *}
+
+definition rtrancl_while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a list) \<Rightarrow> 'a
+  \<Rightarrow> ('a list * 'a set) option"
+where "rtrancl_while p f x =
+  while_option (%(ws,_). ws \<noteq> [] \<and> p(hd ws))
+    ((%(ws,Z).
+     let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
+     in (new @ tl ws, set new \<union> insert x Z)))
+    ([x],{x})"
+
+lemma rtrancl_while_Some: assumes "rtrancl_while p f x = Some(ws,Z)"
+shows "if ws = []
+       then Z = {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z. p z)
+       else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}^* `` {x}"
+proof-
+  let ?test = "(%(ws,_). ws \<noteq> [] \<and> p(hd ws))"
+  let ?step = "(%(ws,Z).
+     let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
+     in (new @ tl ws, set new \<union> insert x Z))"
+  let ?R = "{(x,y). y \<in> set(f x)}"
+  let ?Inv = "%(ws,Z). x \<in> Z \<and> set ws \<subseteq> Z \<and> ?R `` (Z - set ws) \<subseteq> Z \<and>
+                       Z \<subseteq> ?R^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z)"
+  { fix ws Z assume 1: "?Inv(ws,Z)" and 2: "?test(ws,Z)"
+    from 2 obtain v vs where [simp]: "ws = v#vs" by (auto simp: neq_Nil_conv)
+    have "?Inv(?step (ws,Z))" using 1 2
+      by (auto intro: rtrancl.rtrancl_into_rtrancl)
+  } note inv = this
+  hence "!!p. ?Inv p \<Longrightarrow> ?test p \<Longrightarrow> ?Inv(?step p)"
+    apply(tactic {* split_all_tac @{context} 1 *})
+    using inv by iprover
+  moreover have "?Inv ([x],{x})" by (simp)
+  ultimately have I: "?Inv (ws,Z)"
+    by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
+  { assume "ws = []"
+    hence ?thesis using I
+      by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
+  } moreover
+  { assume "ws \<noteq> []"
+    hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
+      by (simp add: subset_iff)
+  }
+  ultimately show ?thesis by simp
+qed
+
 end
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Lifting.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -9,7 +9,7 @@
 imports Equiv_Relations Transfer
 keywords
   "parametric" and
-  "print_quotmaps" "print_quotients" :: diag and
+  "print_quot_maps" "print_quotients" :: diag and
   "lift_definition" :: thy_goal and
   "setup_lifting" :: thy_decl
 begin
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Orderings.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -1230,10 +1230,10 @@
 
 subsection {* Dense orders *}
 
-class inner_dense_order = order +
+class dense_order = order +
   assumes dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
 
-class inner_dense_linorder = linorder + inner_dense_order
+class dense_linorder = linorder + dense_order
 begin
 
 lemma dense_le:
@@ -1312,7 +1312,7 @@
 class no_bot = order + 
   assumes lt_ex: "\<exists>y. y < x"
 
-class dense_linorder = inner_dense_linorder + no_top + no_bot
+class unbounded_dense_linorder = dense_linorder + no_top + no_bot
 
 
 subsection {* Wellorders *}
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -251,7 +251,7 @@
   by (blast intro: borel_open borel_closed)+
 
 lemma open_Collect_less:
-  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
   assumes "continuous_on UNIV f"
   assumes "continuous_on UNIV g"
   shows "open {x. f x < g x}"
@@ -264,14 +264,14 @@
 qed
 
 lemma closed_Collect_le:
-  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
   assumes f: "continuous_on UNIV f"
   assumes g: "continuous_on UNIV g"
   shows "closed {x. f x \<le> g x}"
   using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
 
 lemma borel_measurable_less[measurable]:
-  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows "{w \<in> space M. f w < g w} \<in> sets M"
@@ -285,7 +285,7 @@
 qed
 
 lemma
-  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
   assumes f[measurable]: "f \<in> borel_measurable M"
   assumes g[measurable]: "g \<in> borel_measurable M"
   shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
@@ -755,11 +755,11 @@
   by (simp add: field_divide_inverse)
 
 lemma borel_measurable_max[measurable (raw)]:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
   by (simp add: max_def)
 
 lemma borel_measurable_min[measurable (raw)]:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
   by (simp add: min_def)
 
 lemma borel_measurable_abs[measurable (raw)]:
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Set_Interval.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -373,7 +373,7 @@
 end
 
 
-context inner_dense_linorder
+context dense_linorder
 begin
 
 lemma greaterThanLessThan_empty_iff[simp]:
@@ -519,7 +519,7 @@
 end
 
 lemma
-  fixes x y :: "'a :: {complete_lattice, inner_dense_linorder}"
+  fixes x y :: "'a :: {complete_lattice, dense_linorder}"
   shows Sup_lessThan[simp]: "Sup {..< y} = y"
     and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
     and Sup_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Sup { x <..< y} = y"
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Aug 28 23:48:45 2013 +0200
@@ -25,7 +25,6 @@
     TimedOut |
     Inappropriate |
     OutOfResources |
-    OldSPASS |
     NoPerl |
     NoLibwwwPerl |
     MalformedInput |
@@ -81,7 +80,6 @@
   TimedOut |
   Inappropriate |
   OutOfResources |
-  OldSPASS |
   NoPerl |
   NoLibwwwPerl |
   MalformedInput |
@@ -103,8 +101,7 @@
 
 fun involving [] = ""
   | involving ss =
-    "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
-    " "
+    " involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
 
 fun string_of_failure Unprovable = "The generated problem is unprovable."
   | string_of_failure GaveUp = "The prover gave up."
@@ -114,27 +111,18 @@
     "The prover claims the conjecture is a theorem but provided an incomplete \
     \(or unparsable) proof."
   | string_of_failure (UnsoundProof (false, ss)) =
-    "The prover found an unsound proof " ^ involving ss ^
-    "(or, less likely, your axioms are inconsistent). Specify a sound type \
-    \encoding or omit the \"type_enc\" option."
+    "The prover derived \"False\" using" ^ involving ss ^
+    ". Specify a sound type encoding or omit the \"type_enc\" option."
   | string_of_failure (UnsoundProof (true, ss)) =
-    "The prover found an unsound proof " ^ involving ss ^
-    "(or, less likely, your axioms are inconsistent). Please report this to \
-    \the Isabelle developers."
+    "The prover derived \"False\" using" ^ involving ss ^
+    ". This could be due to inconsistent axioms (including \"sorry\"s) or to \
+    \a bug in Sledgehammer. If the problem persists, please contact the \
+    \Isabelle developers."
   | string_of_failure CantConnect = "Cannot connect to remote server."
   | string_of_failure TimedOut = "Timed out."
   | string_of_failure Inappropriate =
     "The generated problem lies outside the prover's scope."
   | string_of_failure OutOfResources = "The prover ran out of resources."
-  | string_of_failure OldSPASS =
-    "The version of SPASS you are using is obsolete. Please upgrade to \
-    \SPASS 3.8ds. To install it, download and extract the package \
-    \\"http://www21.in.tum.de/~blanchet/spass-3.8ds.tar.gz\" and add the \
-    \\"spass-3.8ds\" directory's absolute path to " ^
-    quote (Path.implode (Path.expand (Path.appends
-               (Path.variable "ISABELLE_HOME_USER" ::
-                map Path.basic ["etc", "components"])))) ^
-    " on a line of its own."
   | string_of_failure NoPerl = "Perl" ^ missing_message_tail
   | string_of_failure NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 28 23:48:45 2013 +0200
@@ -529,8 +529,7 @@
        |> extra_options <> "" ? prefix (extra_options ^ " "),
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
-     [(OldSPASS, "Unrecognized option Isabelle"),
-      (GaveUp, "SPASS beiseite: Completion found"),
+     [(GaveUp, "SPASS beiseite: Completion found"),
       (TimedOut, "SPASS beiseite: Ran out of time"),
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Wed Aug 28 23:48:45 2013 +0200
@@ -6,18 +6,15 @@
 
 signature LIFTING_INFO =
 sig
-  type quotmaps = {rel_quot_thm: thm}
-  val lookup_quotmaps: Proof.context -> string -> quotmaps option
-  val lookup_quotmaps_global: theory -> string -> quotmaps option
-  val print_quotmaps: Proof.context -> unit
-
-  type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
-  type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
-  val transform_quotients: morphism -> quotients -> quotients
-  val lookup_quotients: Proof.context -> string -> quotients option
-  val lookup_quotients_global: theory -> string -> quotients option
-  val update_quotients: string -> quotients -> Context.generic -> Context.generic
-  val dest_quotients: Proof.context -> quotients list
+  type quot_map = {rel_quot_thm: thm}
+  val lookup_quot_maps: Proof.context -> string -> quot_map option
+  val print_quot_maps: Proof.context -> unit
+  
+  type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
+  type quotient = {quot_thm: thm, pcr_info: pcr option}
+  val transform_quotient: morphism -> quotient -> quotient
+  val lookup_quotients: Proof.context -> string -> quotient option
+  val update_quotients: string -> quotient -> Context.generic -> Context.generic
   val print_quotients: Proof.context -> unit
 
   val get_invariant_commute_rules: Proof.context -> thm list
@@ -29,7 +26,10 @@
   type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
     pos_distr_rules: thm list, neg_distr_rules: thm list}
   val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option
-  val lookup_relator_distr_data_global: theory -> string -> relator_distr_data option
+
+  val get_quot_maps           : Proof.context -> quot_map Symtab.table
+  val get_quotients           : Proof.context -> quotient Symtab.table
+  val get_relator_distr_data  : Proof.context -> relator_distr_data Symtab.table
 
   val setup: theory -> theory
 end;
@@ -39,23 +39,62 @@
 
 open Lifting_Util
 
-(** data containers **)
+(** data container **)
+
+type quot_map = {rel_quot_thm: thm}
+type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
+type quotient = {quot_thm: thm, pcr_info: pcr option}
+type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
+  pos_distr_rules: thm list, neg_distr_rules: thm list}
+
+structure Data = Generic_Data
+(
+  type T = 
+    { quot_maps : quot_map Symtab.table,
+      quotients : quotient Symtab.table,
+      reflexivity_rules : thm Item_Net.T,
+      relator_distr_data : relator_distr_data Symtab.table
+    }
+  val empty =
+    { quot_maps = Symtab.empty,
+      quotients = Symtab.empty,
+      reflexivity_rules = Thm.full_rules,
+      relator_distr_data = Symtab.empty
+    }
+  val extend = I
+  fun merge
+    ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1 },
+      { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2 } ) =
+    { quot_maps = Symtab.merge (K true) (qm1, qm2),
+      quotients = Symtab.merge (K true) (q1, q2),
+      reflexivity_rules = Item_Net.merge (rr1, rr2),
+      relator_distr_data = Symtab.merge (K true) (rdd1, rdd2) }
+)
+
+fun map_data f1 f2 f3 f4
+  { quot_maps, quotients, reflexivity_rules, relator_distr_data} =
+  { quot_maps = f1 quot_maps,
+    quotients = f2 quotients,
+    reflexivity_rules = f3 reflexivity_rules,
+    relator_distr_data = f4 relator_distr_data }
+
+fun map_quot_maps           f = map_data f I I I
+fun map_quotients           f = map_data I f I I
+fun map_reflexivity_rules   f = map_data I I f I
+fun map_relator_distr_data  f = map_data I I I f
+  
+val get_quot_maps'           = #quot_maps o Data.get
+val get_quotients'           = #quotients o Data.get
+val get_reflexivity_rules'   = #reflexivity_rules o Data.get
+val get_relator_distr_data'  = #relator_distr_data o Data.get
+
+fun get_quot_maps          ctxt = get_quot_maps' (Context.Proof ctxt)
+fun get_quotients          ctxt = get_quotients' (Context.Proof ctxt)
+fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)
 
 (* info about Quotient map theorems *)
-type quotmaps = {rel_quot_thm: thm}
 
-structure Quotmaps = Generic_Data
-(
-  type T = quotmaps Symtab.table
-  val empty = Symtab.empty
-  val extend = I
-  fun merge data = Symtab.merge (K true) data
-)
-
-val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof
-val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory
-
-(* FIXME export proper internal update operation!? *)
+val lookup_quot_maps = Symtab.lookup o get_quot_maps
 
 fun quot_map_thm_sanity_check rel_quot_thm ctxt =
   let
@@ -102,14 +141,14 @@
     val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs
     val minfo = {rel_quot_thm = rel_quot_thm}
   in
-    Quotmaps.map (Symtab.update (relatorT_name, minfo)) ctxt
+    Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) ctxt
   end    
 
 val quot_map_attribute_setup =
   Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map))
     "declaration of the Quotient map theorem"
 
-fun print_quotmaps ctxt =
+fun print_quot_maps ctxt =
   let
     fun prt_map (ty_name, {rel_quot_thm}) =
       Pretty.block (separate (Pretty.brk 2)
@@ -118,67 +157,49 @@
           Pretty.str "quot. theorem:", 
           Syntax.pretty_term ctxt (prop_of rel_quot_thm)])
   in
-    map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
+    map prt_map (Symtab.dest (get_quot_maps ctxt))
     |> Pretty.big_list "maps for type constructors:"
     |> Pretty.writeln
   end
 
 (* info about quotient types *)
-type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
-type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
-
-structure Quotients = Generic_Data
-(
-  type T = quotients Symtab.table
-  val empty = Symtab.empty
-  val extend = I
-  fun merge data = Symtab.merge (K true) data
-)
-
-fun transform_pcrel_info phi {pcrel_def, pcr_cr_eq} =
+fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} =
   {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}
 
-fun transform_quotients phi {quot_thm, pcrel_info} =
-  {quot_thm = Morphism.thm phi quot_thm, pcrel_info = Option.map (transform_pcrel_info phi) pcrel_info}
+fun transform_quotient phi {quot_thm, pcr_info} =
+  {quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info}
 
-val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
-val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
+fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name
 
-fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
+fun update_quotients type_name qinfo ctxt = 
+  Data.map (map_quotients (Symtab.update (type_name, qinfo))) ctxt
 
 fun delete_quotients quot_thm ctxt =
   let
     val (_, qtyp) = quot_thm_rty_qty quot_thm
     val qty_full_name = (fst o dest_Type) qtyp
-    val symtab = Quotients.get ctxt
-    val opt_stored_quot_thm = Symtab.lookup symtab qty_full_name
+    val symtab = get_quotients' ctxt
+    fun compare_data (_, data) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
   in
-    case opt_stored_quot_thm of
-      SOME data => 
-        if Thm.eq_thm_prop (#quot_thm data, quot_thm) then
-          Quotients.map (Symtab.delete qty_full_name) ctxt
-        else
-          ctxt
-      | NONE => ctxt
+    if Symtab.member compare_data symtab (qty_full_name, quot_thm)
+      then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt
+      else ctxt
   end
 
-fun dest_quotients ctxt =  (* FIXME slightly expensive way to retrieve data *)
-  map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
-
 fun print_quotients ctxt =
   let
-    fun prt_quot (qty_name, {quot_thm, pcrel_info}: quotients) =
+    fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) =
       Pretty.block (separate (Pretty.brk 2)
        [Pretty.str "type:", 
         Pretty.str qty_name,
         Pretty.str "quot. thm:",
         Syntax.pretty_term ctxt (prop_of quot_thm),
         Pretty.str "pcrel_def thm:",
-        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcrel_info,
+        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcr_info,
         Pretty.str "pcr_cr_eq thm:",
-        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcrel_info])
+        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcr_info])
   in
-    map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt)))
+    map prt_quot (Symtab.dest (get_quotients ctxt))
     |> Pretty.big_list "quotients:"
     |> Pretty.writeln
   end
@@ -187,6 +208,8 @@
   Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))
     "deletes the Quotient theorem"
 
+(* theorems that a relator of an invariant is an invariant of the corresponding predicate *)
+
 structure Invariant_Commute = Named_Thms
 (
   val name = @{binding invariant_commute}
@@ -197,16 +220,8 @@
 
 (* info about reflexivity rules *)
 
-structure Reflexivity_Rule = Generic_Data
-(
-  type T = thm Item_Net.T
-  val empty = Thm.full_rules
-  val extend = I
-  val merge = Item_Net.merge
-)
-
-fun get_reflexivity_rules ctxt = ctxt
-  |> (Item_Net.content o Reflexivity_Rule.get o Context.Proof)
+fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt))
+  
 
 (* Conversion to create a reflp' variant of a reflexivity rule  *)
 fun safe_reflp_conv ct =
@@ -219,7 +234,7 @@
       else_conv
       Conv.all_conv) ct
 
-fun add_reflexivity_rule_raw thm = Reflexivity_Rule.map (Item_Net.update thm)
+fun add_reflexivity_rule_raw thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
 val add_reflexivity_rule_raw_attribute = Thm.declaration_attribute add_reflexivity_rule_raw
 
 fun add_reflexivity_rule thm = add_reflexivity_rule_raw thm #>
@@ -230,40 +245,30 @@
 val relfexivity_rule_setup =
   let
     val name = @{binding reflexivity_rule}
-    fun del_thm_raw thm = Reflexivity_Rule.map (Item_Net.remove thm)
+    fun del_thm_raw thm = Data.map (map_reflexivity_rules (Item_Net.remove thm))
     fun del_thm thm = del_thm_raw thm #>
       del_thm_raw (Conv.fconv_rule prep_reflp_conv thm)
     val del = Thm.declaration_attribute del_thm
     val text = "rules that are used to prove that a relation is reflexive"
-    val content = Item_Net.content o Reflexivity_Rule.get
+    val content = Item_Net.content o get_reflexivity_rules'
   in
     Attrib.setup name (Attrib.add_del add_reflexivity_rule_attribute del) text
     #> Global_Theory.add_thms_dynamic (name, content)
   end
 
 (* info about relator distributivity theorems *)
-type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
-  pos_distr_rules: thm list, neg_distr_rules: thm list}
 
-fun map_relator_distr_data f1 f2 f3 f4
+fun map_relator_distr_data' f1 f2 f3 f4
   {pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} =
   {pos_mono_rule   = f1 pos_mono_rule, 
    neg_mono_rule   = f2 neg_mono_rule,
    pos_distr_rules = f3 pos_distr_rules, 
    neg_distr_rules = f4 neg_distr_rules}
 
-fun map_pos_mono_rule f = map_relator_distr_data f I I I
-fun map_neg_mono_rule f = map_relator_distr_data I f I I
-fun map_pos_distr_rules f = map_relator_distr_data I I f I 
-fun map_neg_distr_rules f = map_relator_distr_data I I I f
-
-structure Relator_Distr = Generic_Data
-(
-  type T = relator_distr_data Symtab.table
-  val empty = Symtab.empty
-  val extend = I
-  fun merge data = Symtab.merge (K true) data
-);
+fun map_pos_mono_rule f = map_relator_distr_data' f I I I
+fun map_neg_mono_rule f = map_relator_distr_data' I f I I
+fun map_pos_distr_rules f = map_relator_distr_data' I I f I 
+fun map_neg_distr_rules f = map_relator_distr_data' I I I f
 
 fun introduce_polarities rule =
   let
@@ -315,14 +320,14 @@
     val mono_rule = introduce_polarities mono_rule
     val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
       dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) mono_rule
-    val _ = if Symtab.defined (Relator_Distr.get ctxt) mono_ruleT_name 
+    val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name 
       then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
       else ()
     val neg_mono_rule = negate_mono_rule mono_rule
     val relator_distr_data = {pos_mono_rule = mono_rule, neg_mono_rule = neg_mono_rule, 
       pos_distr_rules = [], neg_distr_rules = []}
   in
-    Relator_Distr.map (Symtab.update (mono_ruleT_name, relator_distr_data)) ctxt
+    Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) ctxt
   end;
 
 local 
@@ -331,8 +336,9 @@
       val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
         dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) distr_rule
     in
-      if Symtab.defined (Relator_Distr.get ctxt) distr_ruleT_name then 
-        Relator_Distr.map (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)) ctxt
+      if Symtab.defined (get_relator_distr_data' ctxt) distr_ruleT_name then 
+        Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule))) 
+          ctxt
       else error "The monoticity rule is not defined."
     end
 
@@ -425,14 +431,13 @@
 
 fun get_distr_rules_raw ctxt = Symtab.fold 
   (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) 
-    (Relator_Distr.get ctxt) []
+    (get_relator_distr_data' ctxt) []
 
 fun get_mono_rules_raw ctxt = Symtab.fold 
   (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) 
-    (Relator_Distr.get ctxt) []
+    (get_relator_distr_data' ctxt) []
 
-val lookup_relator_distr_data = Symtab.lookup o Relator_Distr.get o Context.Proof
-val lookup_relator_distr_data_global = Symtab.lookup o Relator_Distr.get o Context.Theory
+val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data
 
 val relator_distr_attribute_setup =
   Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule))
@@ -456,8 +461,8 @@
 (* outer syntax commands *)
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions"
-    (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
+  Outer_Syntax.improper_command @{command_spec "print_quot_maps"} "print quotient map functions"
+    (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Aug 28 23:48:45 2013 +0200
@@ -201,12 +201,12 @@
     val (pcr_cr_eq, lthy) = case pcrel_def of
       SOME pcrel_def => apfst SOME (define_pcr_cr_eq lthy pcrel_def)
       | NONE => (NONE, lthy)
-    val pcrel_info = case pcrel_def of
+    val pcr_info = case pcrel_def of
       SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
       | NONE => NONE
-    val quotients = { quot_thm = quot_thm, pcrel_info = pcrel_info }
+    val quotients = { quot_thm = quot_thm, pcr_info = pcr_info }
     val qty_full_name = (fst o dest_Type) qtyp  
-    fun quot_info phi = Lifting_Info.transform_quotients phi quotients
+    fun quot_info phi = Lifting_Info.transform_quotient phi quotients
     val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
     val lthy = case opt_reflp_thm of
       SOME reflp_thm => lthy
@@ -376,7 +376,7 @@
       reduced_assm RS thm
     end
 in
-  fun parametrize_domain dom_thm (pcrel_info : Lifting_Info.pcrel_info) ctxt =
+  fun parametrize_domain dom_thm (pcr_info : Lifting_Info.pcr) ctxt =
     let
       fun reduce_first_assm ctxt rules thm =
         let
@@ -386,9 +386,9 @@
           reduced_assm RS thm
         end
 
-      val pcr_cr_met_eq = #pcr_cr_eq pcrel_info RS @{thm eq_reflection}
+      val pcr_cr_met_eq = #pcr_cr_eq pcr_info RS @{thm eq_reflection}
       val pcr_Domainp_eq = rewrite_first_Domainp_arg (Thm.symmetric pcr_cr_met_eq) dom_thm
-      val pcrel_def = #pcrel_def pcrel_info
+      val pcrel_def = #pcrel_def pcr_info
       val pcr_Domainp_par_left_total = 
         (dom_thm RS @{thm pcr_Domainp_par_left_total})
           |> fold_Domainp_pcrel pcrel_def
@@ -422,7 +422,7 @@
 end
 
 fun get_pcrel_info ctxt qty_full_name =  
-  #pcrel_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
+  #pcr_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
 
 fun get_Domainp_thm quot_thm =
    the (get_first (try(curry op RS quot_thm)) [@{thm invariant_to_Domainp}, @{thm Quotient_to_Domainp}])
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Wed Aug 28 23:48:45 2013 +0200
@@ -75,8 +75,8 @@
   end
 
 fun get_pcrel_info ctxt s =
-  case #pcrel_info (get_quot_data ctxt s) of
-    SOME pcrel_info => pcrel_info
+  case #pcr_info (get_quot_data ctxt s) of
+    SOME pcr_info => pcr_info
   | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
     [Pretty.str ("No parametrized correspondce relation for " ^ quote s), 
      Pretty.brk 1, 
@@ -100,7 +100,7 @@
    let
     val thy = Proof_Context.theory_of ctxt
   in
-    (case Lifting_Info.lookup_quotmaps ctxt s of
+    (case Lifting_Info.lookup_quot_maps ctxt s of
       SOME map_data => Thm.transfer thy (#rel_quot_thm map_data)
     | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
       [Pretty.str ("No relator for the type " ^ quote s), 
diff -r 220f306f5c4e -r 082d0972096b src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -567,7 +567,7 @@
   "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
   unfolding eventually_at_top_linorder by auto
 
-lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::dense_linorder. \<forall>n>N. P n)"
+lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::unbounded_dense_linorder. \<forall>n>N. P n)"
   unfolding eventually_at_top_linorder
 proof safe
   fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
@@ -578,7 +578,7 @@
 qed
 
 lemma eventually_gt_at_top:
-  "eventually (\<lambda>x. (c::_::dense_linorder) < x) at_top"
+  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
   unfolding eventually_at_top_dense by auto
 
 definition at_bot :: "('a::order) filter"
@@ -600,7 +600,7 @@
   unfolding eventually_at_bot_linorder by auto
 
 lemma eventually_at_bot_dense:
-  fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
+  fixes P :: "'a::unbounded_dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
   unfolding eventually_at_bot_linorder
 proof safe
   fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
@@ -611,7 +611,7 @@
 qed
 
 lemma eventually_gt_at_bot:
-  "eventually (\<lambda>x. x < (c::_::dense_linorder)) at_bot"
+  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
   unfolding eventually_at_bot_dense by auto
 
 subsection {* Sequentially *}
@@ -794,11 +794,11 @@
 qed
 
 lemma trivial_limit_at_left_real [simp]:
-  "\<not> trivial_limit (at_left (x::'a::{no_bot, dense_linorder, linorder_topology}))"
+  "\<not> trivial_limit (at_left (x::'a::{no_bot, unbounded_dense_linorder, linorder_topology}))"
   unfolding trivial_limit_def eventually_at_left by (auto dest: dense)
 
 lemma trivial_limit_at_right_real [simp]:
-  "\<not> trivial_limit (at_right (x::'a::{no_top, dense_linorder, linorder_topology}))"
+  "\<not> trivial_limit (at_right (x::'a::{no_top, unbounded_dense_linorder, linorder_topology}))"
   unfolding trivial_limit_def eventually_at_right by (auto dest: dense)
 
 lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
@@ -1047,7 +1047,7 @@
   by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
 
 lemma filterlim_at_top_dense:
-  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
+  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
   shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
   by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
             filterlim_at_top[of f F] filterlim_iff[of f at_top F])
@@ -1084,7 +1084,7 @@
 qed
 
 lemma filterlim_at_top_gt:
-  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
+  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
   shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
   by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
 
@@ -1104,7 +1104,7 @@
 qed simp
 
 lemma filterlim_at_bot_lt:
-  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
+  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
   shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
   by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
 
diff -r 220f306f5c4e -r 082d0972096b src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy	Wed Aug 28 23:48:45 2013 +0200
@@ -24,7 +24,7 @@
             (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
 
 lemma interval_empty_iff:
-  "{y. (x::'a::dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
+  "{y. (x::'a::unbounded_dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
   by (auto dest: dense)