# HG changeset patch
# User paulson
# Date 1115044113 -7200
# Node ID f45296bb1485177c1575d3041737e4219e72314b
# Parent  f377ba412dbaf3a62e8fb0f7656746a73bfd42f7
meta-logic connectives now forbidden

diff -r f377ba412dba -r f45296bb1485 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Mon May 02 13:30:48 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Mon May 02 16:28:33 2005 +0200
@@ -217,14 +217,18 @@
 val has_bool_arg_const = 
     exists_Const
       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
+      
+val has_meta_conn = 
+    exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "Goal"]);
   
 (*Raises an exception if any Vars in the theorem mention type bool. That would mean
   they are higher-order, and in addition, they could cause make_horn to loop!
   Functions taking Boolean arguments are also rejected.*)
 fun check_no_bool th =
   let val {prop,...} = rep_thm th
-  in if exists (has_bool o fastype_of) (term_vars prop) orelse
-        has_bool_arg_const prop
+  in if exists (has_bool o fastype_of) (term_vars prop)  orelse
+        has_bool_arg_const prop  orelse  
+        has_meta_conn prop
   then raise THM ("check_no_bool", 0, [th]) else th
   end;