Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
convenience check for vain instantiation
authorhaftmann
Fri, 29 Mar 2013 11:32:07 +0100
changeset 51578 969ad6538b8f
parent 51577 564103cb07d5
child 51579 ec3b78ce0758
convenience check for vain instantiation
src/Pure/Isar/class.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle