# HG changeset patch
# User haftmann
# Date 1364553127 -3600
# Node ID 969ad6538b8fef63f42fef76be08f5bfab6d479a
# Parent  564103cb07d545dfdd76ebd1109649093691cad6
convenience check for vain instantiation

diff -r 564103cb07d5 -r 969ad6538b8f src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Mar 29 13:32:53 2013 +0100
+++ b/src/Pure/Isar/class.ML	Fri Mar 29 11:32:07 2013 +0100
@@ -547,6 +547,9 @@
       then NONE else SOME ((c, tyco),
         (param ^ "_" ^ Long_Name.base_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
     val params = map_product get_param tycos class_params |> map_filter I;
+    val _ = if null params andalso forall (fn tyco => can (Sign.arity_sorts thy tyco) sort) tycos
+      then error "No parameters and no pending instance proof obligations in instantiation."
+      else ();
     val primary_constraints = map (apsnd
       (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
     val algebra = Sign.classes_of thy