make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
authorpaulson
Wed Feb 13 15:14:17 2008 +0100 (2008-02-13)
changeset 2606619df083a2bbf
parent 26065 d80a49f51b94
child 26067 728f2c325ed6
make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
src/HOL/Tools/meson.ML
     1.1 --- a/src/HOL/Tools/meson.ML	Wed Feb 13 10:19:30 2008 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Feb 13 15:14:17 2008 +0100
     1.3 @@ -646,9 +646,13 @@
     1.4  fun negated_asm_of_head th =
     1.5      th RS notEfalse handle THM _ => th RS notEfalse';
     1.6  
     1.7 -(*Converting one clause*)
     1.8 -val make_meta_clause =
     1.9 -  zero_var_indexes o negated_asm_of_head o make_horn resolution_clause_rules;
    1.10 +(*Converting one theorem from a disjunction to a meta-level clause*)
    1.11 +fun make_meta_clause th =
    1.12 +  let val (fth,thaw) = Drule.freeze_thaw_robust th
    1.13 +  in  
    1.14 +      (zero_var_indexes o Thm.varifyT o thaw 0 o 
    1.15 +       negated_asm_of_head o make_horn resolution_clause_rules) fth
    1.16 +  end;
    1.17  
    1.18  fun make_meta_clauses ths =
    1.19      name_thms "MClause#"