# HG changeset patch
# User paulson
# Date 991386230 -7200
# Node ID 416ea5c009f54ff34b5453e42c970b0e719f4eb3
# Parent  908b761cdfb039920726091cdabb7089ab7a0de8
now checks for leading meta-quantifiers and complains, instead of
just raising an exception

diff -r 908b761cdfb0 -r 416ea5c009f5 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu May 31 22:34:58 2001 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Jun 01 11:03:50 2001 +0200
@@ -292,6 +292,9 @@
 
 val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
 
+val all_not_allowed = 
+    "Introduction rule must not have a leading \"!!\" quantifier";
+
 val atomize_cterm = hol_rewrite_cterm inductive_atomize;
 
 in
@@ -307,13 +310,14 @@
       if can HOLogic.dest_Trueprop aprem then ()
       else err_in_prem sg name rule prem "Non-atomic premise";
   in
-    (case HOLogic.dest_Trueprop concl of
-      (Const ("op :", _) $ t $ u) =>
+    (case concl of
+      Const ("Trueprop", _) $ (Const ("op :", _) $ t $ u) =>
         if u mem cs then
           if exists (Logic.occs o rpair t) cs then
             err_in_rule sg name rule "Recursion term on left of member symbol"
           else seq check_prem (prems ~~ aprems)
         else err_in_rule sg name rule bad_concl
+      | Const ("all", _) $ _ => err_in_rule sg name rule all_not_allowed
       | _ => err_in_rule sg name rule bad_concl);
     ((name, arule), att)
   end;