# HG changeset patch
# User wenzelm
# Date 952639103 -3600
# Node ID a8a0411a8e8c1108f2bb5ffef4111573674eedd6
# Parent  84ff2d1f9a2c5967c977f990249fe0a104cbb710
check_case: disallow (T)Vars in invoked case;

diff -r 84ff2d1f9a2c -r a8a0411a8e8c 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