src/HOL/Tools/meson.ML
changeset 15908 f45296bb1485
parent 15872 8336ff711d80
child 15946 94e5f157ab09
equal deleted inserted replaced
15907:f377ba412dba 15908:f45296bb1485
   215 (*True if the term contains a function where the type of any argument contains
   215 (*True if the term contains a function where the type of any argument contains
   216   bool.*)
   216   bool.*)
   217 val has_bool_arg_const = 
   217 val has_bool_arg_const = 
   218     exists_Const
   218     exists_Const
   219       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
   219       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
       
   220       
       
   221 val has_meta_conn = 
       
   222     exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "Goal"]);
   220   
   223   
   221 (*Raises an exception if any Vars in the theorem mention type bool. That would mean
   224 (*Raises an exception if any Vars in the theorem mention type bool. That would mean
   222   they are higher-order, and in addition, they could cause make_horn to loop!
   225   they are higher-order, and in addition, they could cause make_horn to loop!
   223   Functions taking Boolean arguments are also rejected.*)
   226   Functions taking Boolean arguments are also rejected.*)
   224 fun check_no_bool th =
   227 fun check_no_bool th =
   225   let val {prop,...} = rep_thm th
   228   let val {prop,...} = rep_thm th
   226   in if exists (has_bool o fastype_of) (term_vars prop) orelse
   229   in if exists (has_bool o fastype_of) (term_vars prop)  orelse
   227         has_bool_arg_const prop
   230         has_bool_arg_const prop  orelse  
       
   231         has_meta_conn prop
   228   then raise THM ("check_no_bool", 0, [th]) else th
   232   then raise THM ("check_no_bool", 0, [th]) else th
   229   end;
   233   end;
   230 
   234 
   231 (*Create a meta-level Horn clause*)
   235 (*Create a meta-level Horn clause*)
   232 fun make_horn crules th = make_horn crules (tryres(th,crules))
   236 fun make_horn crules th = make_horn crules (tryres(th,crules))