# HG changeset patch
# User wenzelm
# Date 1374090501 -7200
# Node ID f06b403a7dcdb54c1c951e9213fdfce9db7c8ddb
# Parent  8cc7f76b827af0eceda2b2d9bd2a4469a2d99e54# Parent  2fa3110539a50cd908d456a123057724c0fecc73
merged

diff -r 8cc7f76b827a -r f06b403a7dcd src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Wed Jul 17 13:34:21 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Wed Jul 17 21:48:21 2013 +0200
@@ -366,7 +366,12 @@
 fun make_case ctxt config used x clauses =
   let
     fun string_of_clause (pat, rhs) =
-      Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
+      (case try (fn () => (* FIXME may crash!? *)
+        Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs)) ()
+       of
+        SOME s => s
+      | NONE => Markup.markup Markup.intensify "<malformed>");
+
     val _ = map (no_repeat_vars ctxt o fst) clauses;
     val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses;
     val rangeT =
@@ -384,9 +389,11 @@
       (case subtract (op =) tags (map (snd o snd) rows) of
         [] => ()
       | is =>
-          (case config of Error => case_error | Warning => warning | Quiet => fn _ => ())
-            ("The following clauses are redundant (covered by preceding clauses):\n" ^
-              cat_lines (map (string_of_clause o nth clauses) is)));
+          if config = Quiet then ()
+          else
+            (if config = Error then case_error else warning (*FIXME lack of syntactic context!?*))
+              ("The following clauses are redundant (covered by preceding clauses):\n" ^
+                cat_lines (map (string_of_clause o nth clauses) is)));
   in
     case_tm
   end;
diff -r 8cc7f76b827a -r f06b403a7dcd src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Jul 17 21:48:21 2013 +0200
@@ -252,8 +252,6 @@
 
 local
 
-val strict_eq_thm = op = o pairself Thm.rep_thm;
-
 fun apply_att src (context, th) =
   let
     val src1 = Args.assignable src;
@@ -275,7 +273,7 @@
           (case decls of
             [] => [(th, [src'])]
           | (th2, srcs2) :: rest =>
-              if strict_eq_thm (th, th2)
+              if Thm.eq_thm_strict (th, th2)
               then ((th2, src' :: srcs2) :: rest)
               else (th, [src']) :: (th2, srcs2) :: rest);
       in ((th, NONE), (decls', context')) end
@@ -308,7 +306,7 @@
           |>> flat;
         val decls' = rev (map (apsnd rev) decls);
         val facts' =
-          if eq_list (eq_fst strict_eq_thm) (decls', fact') then
+          if eq_list (eq_fst Thm.eq_thm_strict) (decls', fact') then
             [((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')]
           else if null decls' then [((b, []), fact')]
           else [(empty_binding, decls'), ((b, []), fact')];
diff -r 8cc7f76b827a -r f06b403a7dcd src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Jul 17 21:48:21 2013 +0200
@@ -50,8 +50,15 @@
 
 local
 
-fun if_context NONE _ _ = []
-  | if_context (SOME ctxt) f xs = map (f ctxt) xs;
+fun robust f x =
+  (case try f x of
+    SOME s => s
+  | NONE => Markup.markup Markup.intensify "<malformed>");
+
+fun robust2 f x y = robust (fn () => f x y) ();
+
+fun robust_context NONE _ _ = []
+  | robust_context (SOME ctxt) f xs = map (robust2 f ctxt) xs;
 
 fun identify exn =
   let
@@ -96,22 +103,22 @@
             | ERROR msg => msg
             | Fail msg => raised exn "Fail" [msg]
             | THEORY (msg, thys) =>
-                raised exn "THEORY" (msg :: map Context.str_of_thy thys)
+                raised exn "THEORY" (msg :: map (robust Context.str_of_thy) thys)
             | Ast.AST (msg, asts) =>
-                raised exn "AST" (msg :: map (Pretty.string_of o Ast.pretty_ast) asts)
+                raised exn "AST" (msg :: map (robust (Pretty.string_of o Ast.pretty_ast)) asts)
             | TYPE (msg, Ts, ts) =>
                 raised exn "TYPE" (msg ::
-                  (if_context context Syntax.string_of_typ Ts @
-                    if_context context Syntax.string_of_term ts))
+                  (robust_context context Syntax.string_of_typ Ts @
+                    robust_context context Syntax.string_of_term ts))
             | TERM (msg, ts) =>
-                raised exn "TERM" (msg :: if_context context Syntax.string_of_term ts)
+                raised exn "TERM" (msg :: robust_context context Syntax.string_of_term ts)
             | CTERM (msg, cts) =>
                 raised exn "CTERM"
-                  (msg :: if_context context Syntax.string_of_term (map term_of cts))
+                  (msg :: robust_context context Syntax.string_of_term (map term_of cts))
             | THM (msg, i, thms) =>
                 raised exn ("THM " ^ string_of_int i)
-                  (msg :: if_context context Display.string_of_thm thms)
-            | _ => raised exn (Pretty.string_of (pretty_exn exn)) []);
+                  (msg :: robust_context context Display.string_of_thm thms)
+            | _ => raised exn (robust (Pretty.string_of o pretty_exn) exn) []);
         in [((i, msg), id)] end)
       and sorted_msgs context exn =
         sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
diff -r 8cc7f76b827a -r f06b403a7dcd src/Pure/Syntax/type_annotation.ML
--- a/src/Pure/Syntax/type_annotation.ML	Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/Syntax/type_annotation.ML	Wed Jul 17 21:48:21 2013 +0200
@@ -51,12 +51,12 @@
 fun fastype_of Ts (t $ u) =
       (case dest_fun false (fastype_of Ts t) of
         SOME T => T
-      | NONE => raise TERM ("fasfastype_of: expected function type", [t $ u]))
+      | NONE => raise TERM ("fastype_of: expected function type", [t $ u]))
   | fastype_of _ (Const (_, T)) = T
   | fastype_of _ (Free (_, T)) = T
   | fastype_of _ (Var (_, T)) = T
   | fastype_of Ts (Bound i) =
-      (nth Ts i handle General.Subscript => raise TERM ("fasfastype_of: Bound", [Bound i]))
+      (nth Ts i handle General.Subscript => raise TERM ("fastype_of: Bound", [Bound i]))
   | fastype_of Ts (Abs (_, T, u)) = T --> fastype_of (T :: Ts) u;
 
 end;
diff -r 8cc7f76b827a -r f06b403a7dcd src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/System/command_line.ML	Wed Jul 17 21:48:21 2013 +0200
@@ -17,7 +17,11 @@
   uninterruptible (fn restore_attributes => fn () =>
     let val rc =
       restore_attributes body () handle exn =>
-        (Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1);
+        let
+          val _ =
+            Output.error_msg (ML_Compiler.exn_message exn)
+              handle _ => Output.error_msg "Exception raised, but failed to print details!";
+        in if Exn.is_interrupt exn then 130 else 1 end;
     in if rc = 0 then () else exit rc end) ();
 
 fun tool0 body = tool (fn () => (body (); 0));
diff -r 8cc7f76b827a -r f06b403a7dcd src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/context.ML	Wed Jul 17 21:48:21 2013 +0200
@@ -495,7 +495,7 @@
 fun raw_transfer thy' (Proof.Context (data, thy_ref)) =
   let
     val thy = deref thy_ref;
-    val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";
+    val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory";
     val _ = check_thy thy;
     val data' = init_new_data data thy';
     val thy_ref' = check_thy thy';
@@ -518,9 +518,9 @@
   in k end;
 
 fun get k dest prf =
-  dest (case Datatab.lookup (data_of_proof prf) k of
+  (case Datatab.lookup (data_of_proof prf) k of
     SOME x => x
-  | NONE => invoke_init k (Proof_Context.theory_of prf));   (*adhoc value*)
+  | NONE => invoke_init k (Proof_Context.theory_of prf)) |> dest;  (*adhoc value for old theories*)
 
 fun put k mk x = map_prf (Datatab.update (k, mk x));
 
diff -r 8cc7f76b827a -r f06b403a7dcd src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/more_thm.ML	Wed Jul 17 21:48:21 2013 +0200
@@ -39,6 +39,7 @@
   val eq_thm: thm * thm -> bool
   val eq_thm_thy: thm * thm -> bool
   val eq_thm_prop: thm * thm -> bool
+  val eq_thm_strict: thm * thm -> bool
   val equiv_thm: thm * thm -> bool
   val class_triv: theory -> class -> thm
   val of_sort: ctyp * sort -> thm list
@@ -192,6 +193,11 @@
 val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
 val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
 
+fun eq_thm_strict ths =
+  eq_thm_thy ths andalso eq_thm ths andalso
+    let val (rep1, rep2) = pairself Thm.rep_thm ths
+    in #maxidx rep1 = #maxidx rep2 andalso #tags rep1 = #tags rep2 end;
+
 
 (* pattern equivalence *)
 
diff -r 8cc7f76b827a -r f06b403a7dcd src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML	Wed Jul 17 21:48:21 2013 +0200
@@ -32,10 +32,18 @@
 fun not_overloaded_error oconst =
   error ("Constant " ^ quote oconst ^ " is not declared as overloaded");
 
-fun unresolved_overloading_error ctxt (c, T) t reason =
-  error ("Unresolved overloading of " ^ quote c ^ " :: " ^
-    quote (Syntax.string_of_typ ctxt T) ^ " in " ^
-    quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
+fun unresolved_overloading_error ctxt (c, T) t instances =
+  let val ctxt' = Config.put show_variants true ctxt
+  in
+    cat_lines (
+      "Unresolved overloading of constant" ::
+      quote c ^ " :: " ^ quote (Syntax.string_of_typ ctxt' T) ::
+      "in term " ::
+      quote (Syntax.string_of_term ctxt' t) ::
+      (if null instances then "no instances" else "multiple instances:") ::
+    map (Syntax.string_of_term ctxt') instances)
+    |> error
+  end;
 
 (* generic data *)
 
@@ -137,10 +145,13 @@
     handle Type.TUNIFY => NONE
   end;
 
+fun get_instances ctxt (c, T) =
+  Same.function (get_variants ctxt) c
+  |> map_filter (unifiable_with (Proof_Context.theory_of ctxt) T);
+
 fun insert_variants_same ctxt t (Const (c, T)) =
-      (case map_filter (unifiable_with (Proof_Context.theory_of ctxt) T)
-         (Same.function (get_variants ctxt) c) of
-        [] => unresolved_overloading_error ctxt (c, T) t "no instances"
+      (case get_instances ctxt (c, T) of
+        [] => unresolved_overloading_error ctxt (c, T) t []
       | [variant] => variant
       | _ => raise Same.SAME)
   | insert_variants_same _ _ _ = raise Same.SAME;
@@ -173,7 +184,7 @@
     fun check_unresolved t =
       (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of
         [] => ()
-      | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t "multiple instances");
+      | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t (get_instances ctxt (c, T)));
     val _ = map check_unresolved ts;
   in NONE end;
 
diff -r 8cc7f76b827a -r f06b403a7dcd src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Tools/induct.ML	Wed Jul 17 21:48:21 2013 +0200
@@ -162,8 +162,7 @@
   | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
 
 val rearrange_eqs_simproc =
-  Simplifier.simproc_global
-    (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
+  Simplifier.simproc_global Pure.thy "rearrange_eqs" ["all t"]
     (fn ctxt => fn t => mk_swap_rrule ctxt (cterm_of (Proof_Context.theory_of ctxt) t));