check_case: disallow (T)Vars in invoked case;
authorwenzelm
Thu, 09 Mar 2000 22:58:23 +0100
changeset 8403 a8a0411a8e8c
parent 8402 84ff2d1f9a2c
child 8404 4b39358f9810
check_case: disallow (T)Vars in invoked case;
src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 09 22:57:39 2000 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 09 22:58:23 2000 +0100
@@ -828,10 +828,15 @@
 
 (** cases **)
 
+fun check_case ctxt name (xs, ts) =
+  if null (foldr Term.add_typ_tvars (map snd xs, [])) andalso
+    null (foldr Term.add_term_vars (ts, [])) then ()
+  else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt);
+
 fun get_case (ctxt as Context {cases, ...}) name =
   (case Symtab.lookup (cases, name) of
     None => raise CONTEXT ("Unknown case: " ^ quote name, ctxt)
-  | Some c => c);
+  | Some c => (check_case ctxt name c; c));
 
 
 fun add_case (tab, ("", _)) = tab