# HG changeset patch
# User wenzelm
# Date 1324069623 -3600
# Node ID 02cc5fa9c5f1d653a9bc7b146470300b57c52bd6
# Parent  c9ae2bc95fadc7992904087dc07186ebbf8bbfff# Parent  4e70be32621adf7c3eaa6d3ff8f28011cebab272
merged

diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Inductive.thy	Fri Dec 16 22:07:03 2011 +0100
@@ -116,7 +116,7 @@
     to control unfolding*}
 
 lemma def_lfp_unfold: "[| h==lfp(f);  mono(f) |] ==> h = f(h)"
-by (auto intro!: lfp_unfold)
+  by (auto intro!: lfp_unfold)
 
 lemma def_lfp_induct: 
     "[| A == lfp(f); mono(f);
@@ -160,12 +160,12 @@
 
 text{*weak version*}
 lemma weak_coinduct: "[| a: X;  X \<subseteq> f(X) |] ==> a : gfp(f)"
-by (rule gfp_upperbound [THEN subsetD], auto)
+  by (rule gfp_upperbound [THEN subsetD]) auto
 
 lemma weak_coinduct_image: "!!X. [| a : X; g`X \<subseteq> f (g`X) |] ==> g a : gfp f"
-apply (erule gfp_upperbound [THEN subsetD])
-apply (erule imageI)
-done
+  apply (erule gfp_upperbound [THEN subsetD])
+  apply (erule imageI)
+  done
 
 lemma coinduct_lemma:
      "[| X \<le> f (sup X (gfp f));  mono f |] ==> sup X (gfp f) \<le> f (sup X (gfp f))"
@@ -182,7 +182,7 @@
 
 text{*strong version, thanks to Coen and Frost*}
 lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
-by (blast intro: weak_coinduct [OF _ coinduct_lemma])
+  by (blast intro: weak_coinduct [OF _ coinduct_lemma])
 
 lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
   apply (rule order_trans)
@@ -192,7 +192,7 @@
   done
 
 lemma gfp_fun_UnI2: "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))"
-by (blast dest: gfp_lemma2 mono_Un)
+  by (blast dest: gfp_lemma2 mono_Un)
 
 
 subsection {* Even Stronger Coinduction Rule, by Martin Coen *}
@@ -227,27 +227,26 @@
     to control unfolding*}
 
 lemma def_gfp_unfold: "[| A==gfp(f);  mono(f) |] ==> A = f(A)"
-by (auto intro!: gfp_unfold)
+  by (auto intro!: gfp_unfold)
 
 lemma def_coinduct:
      "[| A==gfp(f);  mono(f);  X \<le> f(sup X A) |] ==> X \<le> A"
-by (iprover intro!: coinduct)
+  by (iprover intro!: coinduct)
 
 lemma def_coinduct_set:
      "[| A==gfp(f);  mono(f);  a:X;  X \<subseteq> f(X Un A) |] ==> a: A"
-by (auto intro!: coinduct_set)
+  by (auto intro!: coinduct_set)
 
 (*The version used in the induction/coinduction package*)
 lemma def_Collect_coinduct:
     "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));   
         a: X;  !!z. z: X ==> P (X Un A) z |] ==>  
      a : A"
-apply (erule def_coinduct_set, auto) 
-done
+  by (erule def_coinduct_set) auto
 
 lemma def_coinduct3:
     "[| A==gfp(f); mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"
-by (auto intro!: coinduct3)
+  by (auto intro!: coinduct3)
 
 text{*Monotonicity of @{term gfp}!*}
 lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
@@ -296,8 +295,7 @@
 let
   fun fun_tr ctxt [cs] =
     let
-      (* FIXME proper name context!? *)
-      val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
+      val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
       val ft = Datatype_Case.case_tr true ctxt [x, cs];
     in lambda x ft end
 in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 16 22:07:03 2011 +0100
@@ -644,11 +644,11 @@
               DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
                   (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]);
 
-    val ([dt_induct'], thy7) =
+    val ([(_, [dt_induct'])], thy7) =
       thy6
-      |> Global_Theory.add_thms
-        [((Binding.qualify true big_name (Binding.name "induct"), dt_induct),
-          [case_names_induct])]
+      |> Global_Theory.note_thmss ""
+        [((Binding.qualify true big_name (Binding.name "induct"), [case_names_induct]),
+          [([dt_induct], [])])]
       ||> Theory.checkpoint;
 
   in
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Dec 16 22:07:03 2011 +0100
@@ -233,7 +233,7 @@
         (if length descr' = 1 then [big_reccomb_name]
          else map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr'));
     val reccombs =
-      map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
+      map (fn ((name, T), T') => Const (name, reccomb_fn_Ts @ [T] ---> T'))
         (reccomb_names ~~ recTs ~~ rec_result_Ts);
 
     val (reccomb_defs, thy2) =
@@ -245,9 +245,9 @@
           (map
             (fn ((((name, comb), set), T), T') =>
               (Binding.name (Long_Name.base_name name ^ "_def"),
-                Logic.mk_equals (comb, absfree ("x", T)
+                Logic.mk_equals (comb, fold_rev lambda rec_fns (absfree ("x", T)
                  (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
-                   (set $ Free ("x", T) $ Free ("y", T'))))))
+                   (set $ Free ("x", T) $ Free ("y", T')))))))
             (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
       ||> Sign.parent_path
       ||> Theory.checkpoint;
@@ -270,10 +270,11 @@
   in
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
-    |> Global_Theory.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])]
+    |> Global_Theory.note_thmss ""
+      [((Binding.name "recs", [Nitpick_Simps.add]), [(rec_thms, [])])]
     ||> Sign.parent_path
     ||> Theory.checkpoint
-    |-> (fn thms => pair (reccomb_names, flat thms))
+    |-> (fn thms => pair (reccomb_names, maps #2 thms))
   end;
 
 
@@ -324,9 +325,10 @@
             val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
             val def =
               (Binding.name (Long_Name.base_name name ^ "_def"),
-                Logic.mk_equals (list_comb (Const (name, caseT), fns1),
-                  list_comb (reccomb, (flat (take i case_dummy_fns)) @
-                    fns2 @ (flat (drop (i + 1) case_dummy_fns)))));
+                Logic.mk_equals (Const (name, caseT),
+                  fold_rev lambda fns1
+                    (list_comb (reccomb,
+                      flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
             val ([def_thm], thy') =
               thy
               |> Sign.declare_const_global decl |> snd
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 16 22:07:03 2011 +0100
@@ -93,29 +93,29 @@
 
 (* store theorems in theory *)
 
-fun store_thmss_atts label tnames attss thmss =
+fun store_thmss_atts name tnames attss thmss =
   fold_map (fn ((tname, atts), thms) =>
-    Global_Theory.add_thmss
-      [((Binding.qualify true tname (Binding.name label), thms), atts)]
-    #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
+    Global_Theory.note_thmss ""
+      [((Binding.qualify true tname (Binding.name name), atts), [(thms, [])])]
+    #-> (fn [(_, res)] => pair res)) (tnames ~~ attss ~~ thmss)
   ##> Theory.checkpoint;
 
-fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
+fun store_thmss name tnames = store_thmss_atts name tnames (replicate (length tnames) []);
 
-fun store_thms_atts label tnames attss thmss =
-  fold_map (fn ((tname, atts), thms) =>
-    Global_Theory.add_thms
-      [((Binding.qualify true tname (Binding.name label), thms), atts)]
-    #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
+fun store_thms_atts name tnames attss thms =
+  fold_map (fn ((tname, atts), thm) =>
+    Global_Theory.note_thmss ""
+      [((Binding.qualify true tname (Binding.name name), atts), [([thm], [])])]
+    #-> (fn [(_, [res])] => pair res)) (tnames ~~ attss ~~ thms)
   ##> Theory.checkpoint;
 
-fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
+fun store_thms name tnames = store_thms_atts name tnames (replicate (length tnames) []);
 
 
 (* split theorem thm_1 & ... & thm_n into n theorems *)
 
 fun split_conj_thm th =
-  ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
+  ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
 
 val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj});
 val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj});
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Dec 16 22:07:03 2011 +0100
@@ -78,25 +78,26 @@
     val dt_names = map fst dt_infos;
     val prfx = Binding.qualify true (space_implode "_" new_type_names);
     val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;
-    val named_rules = flat (map_index (fn (index, tname) =>
-      [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
-       ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
+    val named_rules = flat (map_index (fn (i, tname) =>
+      [((Binding.empty, [Induct.induct_type tname]), [([nth inducts i], [])]),
+       ((Binding.empty, [Induct.cases_type tname]), [([nth exhaust i], [])])]) dt_names);
     val unnamed_rules = map (fn induct =>
-      ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
+      ((Binding.empty, [Rule_Cases.inner_rule, Induct.induct_type ""]), [([induct], [])]))
         (drop (length dt_names) inducts);
   in
     thy9
-    |> Global_Theory.add_thmss ([((prfx (Binding.name "simps"), simps), []),
-        ((prfx (Binding.name "inducts"), inducts), []),
-        ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
-        ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites),
-          [Simplifier.simp_add]),
-        ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
-        ((Binding.empty, flat inject), [iff_add]),
-        ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
-          [Classical.safe_elim NONE]),
-        ((Binding.empty, weak_case_congs), [Simplifier.cong_add]),
-        ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @
+    |> Global_Theory.note_thmss ""
+      ([((prfx (Binding.name "simps"), []), [(simps, [])]),
+        ((prfx (Binding.name "inducts"), []), [(inducts, [])]),
+        ((prfx (Binding.name "splits"), []), [(maps (fn (x, y) => [x, y]) splits, [])]),
+        ((Binding.empty, [Simplifier.simp_add]),
+          [(flat case_rewrites @ flat distinct @ rec_rewrites, [])]),
+        ((Binding.empty, [Code.add_default_eqn_attribute]), [(rec_rewrites, [])]),
+        ((Binding.empty, [iff_add]), [(flat inject, [])]),
+        ((Binding.empty, [Classical.safe_elim NONE]),
+          [(map (fn th => th RS notE) (flat distinct), [])]),
+        ((Binding.empty, [Simplifier.cong_add]), [(weak_case_congs, [])]),
+        ((Binding.empty, [Induct.induct_simp_add]), [(flat (distinct @ inject), [])])] @
           named_rules @ unnamed_rules)
     |> snd
     |> Datatype_Data.register dt_infos
@@ -116,13 +117,13 @@
     val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
     val new_type_names = map Long_Name.base_name dt_names;
     val prfx = Binding.qualify true (space_implode "_" new_type_names);
-    val (((inject, distinct), [induct]), thy2) =
+    val (((inject, distinct), [(_, [induct])]), thy2) =
       thy1
       |> Datatype_Aux.store_thmss "inject" new_type_names raw_inject
       ||>> Datatype_Aux.store_thmss "distinct" new_type_names raw_distinct
-      ||>> Global_Theory.add_thms
-        [((prfx (Binding.name "induct"), raw_induct),
-          [Datatype_Data.mk_case_names_induct descr])];
+      ||>> Global_Theory.note_thmss ""
+        [((prfx (Binding.name "induct"), [Datatype_Data.mk_case_names_induct descr]),
+          [([raw_induct], [])])];
   in
     thy2
     |> derive_datatype_props config dt_names [descr] induct inject distinct
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Tools/Function/size.ML	Fri Dec 16 22:07:03 2011 +0100
@@ -202,12 +202,12 @@
     val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
       prove_size_eqs Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
 
-    val ([size_thms], thy'') =
-      Global_Theory.add_thmss
-        [((Binding.name "size", size_eqns),
-          [Simplifier.simp_add, Nitpick_Simps.add,
-           Thm.declaration_attribute
-               (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy';
+    val ([(_, size_thms)], thy'') = thy'
+      |> Global_Theory.note_thmss ""
+        [((Binding.name "size",
+            [Simplifier.simp_add, Nitpick_Simps.add,
+             Thm.declaration_attribute (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
+          [(size_eqns, [])])];
 
   in
     SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Pure/General/scan.scala	Fri Dec 16 22:07:03 2011 +0100
@@ -79,7 +79,7 @@
 
     /* pseudo Set methods */
 
-    def iterator: Iterator[String] = content(main_tree, Nil).sortWith(_ <= _).iterator
+    def iterator: Iterator[String] = content(main_tree, Nil).sorted.iterator
 
     override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
 
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 16 22:07:03 2011 +0100
@@ -183,8 +183,7 @@
             for (imp <- header.imports; name <- names.get(imp)) yield(name)
           case Exn.Exn(_) => Nil
         }
-      Library.topological_order(next,
-        Library.sort_wrt((name: Node.Name) => name.node, nodes.keys.toList))
+      Library.topological_order(next, nodes.keys.toList.sortBy(_.node))
     }
   }
 
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Dec 16 22:07:03 2011 +0100
@@ -297,7 +297,7 @@
         for (file <- files if file.isFile) logics += file.getName
       }
     }
-    logics.toList.sortWith(_ < _)
+    logics.toList.sorted
   }
 
 
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Pure/Thy/completion.scala	Fri Dec 16 22:07:03 2011 +0100
@@ -96,7 +96,7 @@
           case Some(word) =>
             words_lex.completions(word).map(words_map(_)) match {
               case Nil => None
-              case cs => Some(word, cs.sortWith(_ < _))
+              case cs => Some(word, cs.sorted)
             }
           case None => None
         }
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Pure/library.scala	Fri Dec 16 22:07:03 2011 +0100
@@ -64,18 +64,6 @@
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
-  def sort_wrt[A](key: A => String, args: Seq[A]): List[A] =
-  {
-    val ordering: Ordering[A] =
-      new Ordering[A] { def compare(x: A, y: A): Int = key(x) compare key(y) }
-    val a = (new Array[Any](args.length)).asInstanceOf[Array[A]]
-    for ((x, i) <- args.iterator zipWithIndex) a(i) = x
-    Sorting.quickSort[A](a)(ordering)
-    a.toList
-  }
-
-  def sort_strings(args: Seq[String]): List[String] = sort_wrt((x: String) => x, args)
-
 
   /* iterate over chunks (cf. space_explode) */
 
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Dec 16 22:07:03 2011 +0100
@@ -96,7 +96,7 @@
             case Some((word, cs)) =>
               val ds =
                 (if (Isabelle_Encoding.is_active(buffer))
-                  cs.map(Symbol.decode(_)).sortWith(_ < _)
+                  cs.map(Symbol.decode(_)).sorted
                  else cs).filter(_ != word)
               if (ds.isEmpty) null
               else new SideKickCompletion(
diff -r c9ae2bc95fad -r 02cc5fa9c5f1 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Dec 16 22:07:03 2011 +0100
@@ -379,7 +379,7 @@
         filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
 
       if (!files.isEmpty) {
-        val files_list = new ListView(Library.sort_strings(files))
+        val files_list = new ListView(files.sorted)
         for (i <- 0 until files.length)
           files_list.selection.indices += i