src/HOL/Tools/meson.ML
changeset 15908 f45296bb1485
parent 15872 8336ff711d80
child 15946 94e5f157ab09
--- 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;