# HG changeset patch
# User wenzelm
# Date 821717230 -3600
# Node ID 1f5949a43e8297b92bf1eb8ce74744d96b27dc00
# Parent  3cc22794ce719417f25016e0f454a4bba98a35a2
improved printing of errors in 'defs';
fixed small bug in 'standard' (it used to fail stripping shyps in some cases);

diff -r 3cc22794ce71 -r 1f5949a43e82 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Jan 15 15:00:14 1996 +0100
+++ b/src/Pure/drule.ML	Mon Jan 15 15:47:10 1996 +0100
@@ -190,7 +190,7 @@
       [Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty]));
 
     fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn;
-    fun show_defns c = commas o map (show_defn c);
+    fun show_defns c = cat_lines o map (show_defn c);
 
     val (c, ty) = dest_defn tm
       handle TERM (msg, _) => err_in_defn name msg;
@@ -198,7 +198,7 @@
   in
     if not (null defns) then
       err_in_defn name ("Definition of " ^ show_const (c, ty) ^
-        " clashes with " ^ show_defns c defns)
+        "\nclashes with " ^ show_defns c defns)
     else (name, tm) :: axms
   end;
 
@@ -541,8 +541,8 @@
   let val {maxidx,...} = rep_thm th
   in
     th |> implies_intr_hyps
-       |> Thm.strip_shyps |> implies_intr_shyps
        |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
+       |> Thm.strip_shyps |> Thm.implies_intr_shyps
        |> zero_var_indexes |> Thm.varifyT |> Thm.compress
   end;