now checks for leading meta-quantifiers and complains, instead of
authorpaulson
Fri Jun 01 11:03:50 2001 +0200 (2001-06-01 ago)
changeset 11358416ea5c009f5
parent 11357 908b761cdfb0
child 11359 29f8b00d7e1f
now checks for leading meta-quantifiers and complains, instead of
just raising an exception
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu May 31 22:34:58 2001 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jun 01 11:03:50 2001 +0200
     1.3 @@ -292,6 +292,9 @@
     1.4  
     1.5  val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
     1.6  
     1.7 +val all_not_allowed = 
     1.8 +    "Introduction rule must not have a leading \"!!\" quantifier";
     1.9 +
    1.10  val atomize_cterm = hol_rewrite_cterm inductive_atomize;
    1.11  
    1.12  in
    1.13 @@ -307,13 +310,14 @@
    1.14        if can HOLogic.dest_Trueprop aprem then ()
    1.15        else err_in_prem sg name rule prem "Non-atomic premise";
    1.16    in
    1.17 -    (case HOLogic.dest_Trueprop concl of
    1.18 -      (Const ("op :", _) $ t $ u) =>
    1.19 +    (case concl of
    1.20 +      Const ("Trueprop", _) $ (Const ("op :", _) $ t $ u) =>
    1.21          if u mem cs then
    1.22            if exists (Logic.occs o rpair t) cs then
    1.23              err_in_rule sg name rule "Recursion term on left of member symbol"
    1.24            else seq check_prem (prems ~~ aprems)
    1.25          else err_in_rule sg name rule bad_concl
    1.26 +      | Const ("all", _) $ _ => err_in_rule sg name rule all_not_allowed
    1.27        | _ => err_in_rule sg name rule bad_concl);
    1.28      ((name, arule), att)
    1.29    end;