reverted to verion from fc27be4c6b1c

--- a/src/Tools/Code/code_thingol.ML	Fri Jul 02 16:15:49 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Jul 02 16:20:56 2010 +0200
@@ -86,7 +86,6 @@
   val is_case: stmt -> bool
   val contr_classparam_typs: program -> string -> itype option list
   val labelled_name: theory -> program -> string -> string
-  val labelled_traceback: theory -> program -> string -> string
   val group_stmts: theory -> program
     -> ((string * stmt) list * (string * stmt) list
       * ((string * stmt) list * (string * stmt) list)) list
@@ -490,15 +489,6 @@
         val Datatype (tyco, _) = Graph.get_node program tyco
       in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
 
-fun labelled_traceback thy program name =
-  let
-    val minimals = Graph.minimals program;
-    val traceback = these (get_first
-      (fn minimal => case Graph.irreducible_paths program (minimal, name)
-        of [] => NONE
-         | p :: ps => SOME p) minimals);
-  in space_implode " -> " (map (labelled_name thy program) traceback) end;
-
 fun linear_stmts program =
   rev (Graph.strong_conn program)
   |> map (AList.make (Graph.get_node program));
@@ -557,19 +547,21 @@
 
 exception PERMISSIVE of unit;
 
-fun translation_error thy permissive some_thm msg sub_msg (dep, (_, program)) =
+fun translation_error thy permissive some_thm msg sub_msg =
   if permissive
   then raise PERMISSIVE ()
   else let
     val err_thm = case some_thm
      of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
       | NONE => "";
-    val traceback = case dep
-     of SOME name => labelled_traceback thy program name
-      | NONE => "";
-    val err_traceback = if traceback = ""
-      then "" else "\n(dependencies " ^ traceback ^ ")";
-  in error (msg ^ err_thm ^ err_traceback ^ ":\n" ^ sub_msg) end;
+  in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
+
+fun not_wellsorted thy permissive some_thm ty sort e =
+  let
+    val err_class = Sorts.class_error (Syntax.pp_global thy) e;
+    val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
+      ^ Syntax.string_of_sort_global thy sort;
+  in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
 
 
 (* translation *)
@@ -706,15 +698,16 @@
     handle PERMISSIVE () => ([], prgrm)
 and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
   let
-    val abstraction_violation = (case some_abs of NONE => true | SOME abs => not (c = abs))
+    val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
         andalso Code.is_abstr thy c
+        then translation_error thy permissive some_thm
+          "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
+      else ()
     val arg_typs = Sign.const_typargs thy (c, ty);
     val sorts = Code_Preproc.sortargs eqngr c;
     val function_typs = (fst o Term.strip_type) ty;
   in
-    abstraction_violation ? translation_error thy permissive some_thm
-      "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
-    #> ensure_const thy algbr eqngr permissive c
+    ensure_const thy algbr eqngr permissive c
     ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
     ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
     ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs
@@ -803,12 +796,6 @@
   #>> (fn sort => (unprefix "'" v, sort))
 and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) =
   let
-    fun format_class_error e =
-      let
-        val err_class = Sorts.class_error (Syntax.pp_global thy) e;
-        val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
-          ^ Syntax.string_of_sort_global thy sort;
-      in err_typ ^ "\n" ^ err_class end;
     datatype typarg =
         Global of (class * string) * typarg list list
       | Local of (class * class) list * (string * (int * sort));
@@ -822,11 +809,11 @@
       let
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
-    val (class_error, typargs) = ("", Sorts.of_sort_derivation algebra
+    val typargs = Sorts.of_sort_derivation algebra
       {class_relation = K (Sorts.classrel_derivation algebra class_relation),
        type_constructor = type_constructor,
-       type_variable = type_variable} (ty, proj_sort sort))
-      handle Sorts.CLASS_ERROR e => (format_class_error e, []);
+       type_variable = type_variable} (ty, proj_sort sort)
+      handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e;
     fun mk_dict (Global (inst, yss)) =
           ensure_inst thy algbr eqngr permissive inst
           ##>> (fold_map o fold_map) mk_dict yss
@@ -834,11 +821,7 @@
       | mk_dict (Local (classrels, (v, (n, sort)))) =
           fold_map (ensure_classrel thy algbr eqngr permissive) classrels
           #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort))))
-  in
-    not (class_error = "")
-      ? translation_error thy permissive some_thm "Wellsortedness error" class_error
-    #> fold_map mk_dict typargs
-  end;
+  in fold_map mk_dict typargs end;
 
 
 (* store *)