# HG changeset patch
# User haftmann
# Date 1197364992 -3600
# Node ID 35a5f7f4b97b9e15a8ed87c0c9a5b15e44afa63e
# Parent  6c1714b9b805a80058009771cbbab31b2ff49893
error handling for pathological cases

diff -r 6c1714b9b805 -r 35a5f7f4b97b src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Dec 11 10:23:11 2007 +0100
+++ b/src/Pure/axclass.ML	Tue Dec 11 10:23:12 2007 +0100
@@ -327,8 +327,13 @@
 
 fun declare_overloaded (c, T) thy =
   let
-    val SOME class = class_of_param thy c;
-    val SOME tyco = inst_tyco_of thy (c, T);
+    val class = case class_of_param thy c
+     of SOME class => class
+      | NONE => error ("Not a class parameter: " ^ quote c);
+    val tyco = case inst_tyco_of thy (c, T)
+     of SOME tyco => tyco
+      | NONE => error ("Illegal type for instantiation of class parameter: "
+        ^ quote (c ^ " :: " ^ Sign.string_of_typ thy T));
     val name_inst = instance_name (tyco, class) ^ "_inst";
     val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
     val T' = Type.strip_sorts T;