tuned;

--- a/src/Pure/Isar/ROOT.ML	Tue Apr 25 22:23:30 2006 +0200
+++ b/src/Pure/Isar/ROOT.ML	Tue Apr 25 22:23:41 2006 +0200
@@ -36,10 +36,10 @@
 use "calculation.ML";
 use "obtain.ML";
 use "locale.ML";
+use "../axclass.ML";
 use "local_theory.ML";
 use "specification.ML";
 use "constdefs.ML";
-use "../axclass.ML";
 
 (*outer syntax*)
 use "antiquote.ML";

--- a/src/Pure/Isar/element.ML	Tue Apr 25 22:23:30 2006 +0200
+++ b/src/Pure/Isar/element.ML	Tue Apr 25 22:23:41 2006 +0200
@@ -326,12 +326,11 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val th = Goal.norm_hhf raw_th;
-    val maxidx = #maxidx (Thm.rep_thm th);
 
     fun standard_thesis t =
       let
         val C = ObjectLogic.drop_judgment thy (Thm.concl_of th);
-        val C' = Var ((AutoBind.thesisN, maxidx + 1), Term.fastype_of C);
+        val C' = Var ((AutoBind.thesisN, Thm.maxidx_of th + 1), Term.fastype_of C);
       in Term.subst_atomic [(C, C')] t end;
 
     val raw_prop =

--- a/src/Pure/Proof/extraction.ML	Tue Apr 25 22:23:30 2006 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Apr 25 22:23:41 2006 +0200
@@ -101,7 +101,7 @@
       in
         get_first (fn (_, (prems, (tm1, tm2))) =>
         let
-          fun ren t = getOpt (Term.rename_abs tm1 tm t, t);
+          fun ren t = the_default t (Term.rename_abs tm1 tm t);
           val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
           val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
           val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
@@ -463,7 +463,7 @@
     val procs = List.concat (map (fst o snd) types);
     val rtypes = map fst types;
     val typroc = typeof_proc (Sign.defaultS thy');
-    val prep = getOpt (prep, K I) thy' o ProofRewriteRules.elim_defs thy' false defs o
+    val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o
       Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand);
     val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
 

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Apr 25 22:23:30 2006 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Apr 25 22:23:41 2006 +0200
@@ -231,7 +231,7 @@
               val (_, rhs) = Logic.dest_equals prop;
               val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
                 (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs),
-                map valOf ts);
+                map the ts);
             in
               change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
             end

--- a/src/Pure/Tools/codegen_package.ML	Tue Apr 25 22:23:30 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Tue Apr 25 22:23:41 2006 +0200
@@ -164,7 +164,7 @@
                 NameSpace.drop_base c';
       val c'' = NameSpace.append prefix (NameSpace.base c');
       fun mangle (Type (tyco, tys)) =
-            (NameSpace.base o alias_get thy) tyco :: Library.flat (List.mapPartial mangle tys) |> SOME
+            (NameSpace.base o alias_get thy) tyco :: flat (List.mapPartial mangle tys) |> SOME
         | mangle _ =
             NONE
     in
@@ -172,7 +172,7 @@
       |> Type.raw_match (Sign.the_const_type thy c, ty)
       |> map (snd o snd) o Vartab.dest
       |> List.mapPartial mangle
-      |> Library.flat
+      |> flat
       |> null ? K ["x"]
       |> cons c''
       |> space_implode "_"
@@ -959,7 +959,7 @@
                 in map_atyps (fn _ => ty_inst) ty end;
               val tys =
                 (Type.logical_types o Sign.tsig_of) thy
-                |> filter (fn tyco => (is_some oo try) (Sorts.mg_domain (Sign.classes_of thy, Sign.arities_of thy) tyco) (Sign.defaultS thy))
+                |> filter (fn tyco => can (Sign.arity_sorts thy tyco) (Sign.defaultS thy))
                 |> map inst
             in
               (overltab1
@@ -1027,7 +1027,7 @@
             then I
             else cons (name, NameSpace.append thyname (NameSpace.base name))) names [];
       in diff names end;
-    val inconsistent = map get_inconsistent (ThyInfo.names ()) |> Library.flat;
+    val inconsistent = map get_inconsistent (ThyInfo.names ()) |> flat;
     fun add (src, dst) thy =
       if (is_some oo Symtab.lookup o fst o #alias o #logic_data o CodegenData.get) thy src
       then (warning ("code generator alias already defined for " ^ quote src ^ ", will not overwrite"); thy)

--- a/src/Pure/Tools/codegen_serializer.ML	Tue Apr 25 22:23:30 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Apr 25 22:23:41 2006 +0200
@@ -892,7 +892,7 @@
       in 
         vs
         |> map (fn (v, sort) => map (pair v) sort)
-        |> Library.flat
+        |> flat
         |> from_sctxt
       end;
     fun hs_from_tycoexpr fxy (tyco, tys) =

--- a/src/Pure/Tools/codegen_theorems.ML	Tue Apr 25 22:23:30 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML	Tue Apr 25 22:23:41 2006 +0200
@@ -441,7 +441,7 @@
      of [] =>
           Defs.specifications_of (Theory.defs_of thy) c
           |> map (PureThy.get_thms thy o Name o fst o snd)
-          |> Library.flat
+          |> flat
           |> append (getf_first_list (map (fn f => f thy) (the_funs_extrs thy)) (c, ty))
           |> map (dest_fun thy)
           |> filter_typ

--- a/src/Pure/Tools/codegen_thingol.ML	Tue Apr 25 22:23:30 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Tue Apr 25 22:23:41 2006 +0200
@@ -715,7 +715,7 @@
             (the_default empty_module o Option.map dest_modl o try (Graph.get_node modl2)) name)
     and diff_modl prefix (modl1, modl2) =
       fold (diff_entry prefix modl2)
-        ((AList.make (Graph.get_node modl1) o Library.flat o Graph.strong_conn) modl1)
+        ((AList.make (Graph.get_node modl1) o flat o Graph.strong_conn) modl1)
   in diff_modl [] modl12 [] end;
 
 local 
@@ -768,7 +768,7 @@
     |> imports [] name 
     (*|> cons name
     |> map (fn name => submodules name (get_modl name) [])
-    |> Library.flat
+    |> flat
     |> remove (op =) name*)
     |> map NameSpace.pack
   end;