tuned;

--- a/src/HOL/Tools/inductive_package.ML	Fri Oct 06 15:39:29 2006 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 07 01:30:58 2006 +0200
@@ -138,7 +138,7 @@
         | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
     val concl = concl_of thm
   in
-    if Logic.is_equals concl then
+    if can Logic.dest_equals concl then
       eq2mono (thm RS meta_eq_to_obj_eq)
     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
       eq2mono thm

--- a/src/HOL/simpdata.ML	Fri Oct 06 15:39:29 2006 +0200
+++ b/src/HOL/simpdata.ML	Sat Oct 07 01:30:58 2006 +0200
@@ -272,7 +272,7 @@
   (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
      rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
    in mk_meta_eq rl' handle THM _ =>
-     if Logic.is_equals (concl_of rl') then rl'
+     if can Logic.dest_equals (concl_of rl') then rl'
      else error "Conclusion of congruence rules must be =-equality"
    end);
 

--- a/src/Pure/Isar/locale.ML	Fri Oct 06 15:39:29 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Oct 07 01:30:58 2006 +0200
@@ -898,7 +898,7 @@
         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
             let val ((c, _), t') = LocalDefs.cert_def ctxt t
-            in (t', ((if name = "" then Thm.def_name c else name, atts), [(t', ps)])) end);
+            in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
         val (_, ctxt') =
           ctxt |> fold (Variable.fix_frees o #1) asms
           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
@@ -1455,13 +1455,10 @@
 (* print locale *)
 
 fun print_locale thy show_facts import body =
-  let
-    val (all_elems, ctxt) = read_expr import body (ProofContext.init thy);
-    val prt_elem = Element.pretty_ctxt ctxt;
-  in
+  let val (all_elems, ctxt) = read_expr import body (ProofContext.init thy) in
     Pretty.big_list "locale elements:" (all_elems
       |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
-      |> map (Pretty.chunks o prt_elem))
+      |> map (Pretty.chunks o Element.pretty_ctxt ctxt))
     |> Pretty.writeln
   end;
 

--- a/src/Pure/Isar/proof.ML	Fri Oct 06 15:39:29 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Oct 07 01:30:58 2006 +0200
@@ -557,7 +557,7 @@
     val ((raw_names, raw_atts), (vars, raw_rhss)) =
       args |> split_list |>> split_list ||> split_list;
     val xs = map #1 vars;
-    val names = map (fn ("", x) => Thm.def_name x | (name, _) => name) (raw_names ~~ xs);
+    val names = map2 Thm.def_name_optional xs raw_names;
     val atts = map (map (prep_att thy)) raw_atts;
     val (rhss, state') = state |> map_context_result (prep_binds false (map swap raw_rhss));
     val eqs = LocalDefs.mk_def (context_of state') (xs ~~ rhss);

--- a/src/Pure/old_goals.ML	Fri Oct 06 15:39:29 2006 +0200
+++ b/src/Pure/old_goals.ML	Sat Oct 07 01:30:58 2006 +0200
@@ -156,7 +156,7 @@
       val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
       val (As, B) = Logic.strip_horn horn;
       val atoms = atomic andalso
-            forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
+            forall (fn t => not (can Logic.dest_implies t orelse Logic.is_all t)) As;
       val (As,B) = if atoms then ([],horn) else (As,B);
       val cAs = map (cterm_of thy) As;
       val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs;

--- a/src/Pure/simplifier.ML	Fri Oct 06 15:39:29 2006 +0200
+++ b/src/Pure/simplifier.ML	Sat Oct 07 01:30:58 2006 +0200
@@ -335,7 +335,7 @@
     val safe_solver = mk_solver "easy safe" safe_solver_tac;
 
     fun mk_eq thm =
-      if Logic.is_equals (Thm.concl_of thm) then [thm]
+      if can Logic.dest_equals (Thm.concl_of thm) then [thm]
       else [thm RS reflect] handle THM _ => [];
 
     fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);